(* Author: Andreas Lochbihler, ETH Zurich Author: Florian Haftmann, TU Muenchen with some material ported from HOL Light by LCP
*)
section \<open>Polynomial mapping: combination of almost everywhere zero functions with an algebraic view\<close>
theory Poly_Mapping imports Groups_Big_Fun Fun_Lexorder More_List begin
subsection \<open>Preliminary: auxiliary operations for \emph{almost everywhere zero}\<close>
text\<open>
A central notion for polynomials are functions being \emph{almost everywhere zero}. For these we provide some auxiliary definitions andlemmas. \<close>
lemma finite_mult_not_eq_zero_leftI: fixes f :: "'b \ 'a :: mult_zero" assumes"finite {a. f a \ 0}" shows"finite {a. g a * f a \ 0}" by (metis (mono_tags, lifting) Collect_mono assms mult_zero_right finite_subset)
lemma finite_mult_not_eq_zero_rightI: fixes f :: "'b \ 'a :: mult_zero" assumes"finite {a. f a \ 0}" shows"finite {a. f a * g a \ 0}" by (metis (mono_tags, lifting) Collect_mono assms lambda_zero finite_subset)
lemma finite_mult_not_eq_zero_prodI: fixes f g :: "'a \ 'b::semiring_0" assumes"finite {a. f a \ 0}" (is "finite ?F") assumes"finite {b. g b \ 0}" (is "finite ?G") shows"finite {(a, b). f a * g b \ 0}" proof - from assms have"finite (?F \ ?G)" by blast thenhave"finite {(a, b). f a \ 0 \ g b \ 0}" by simp thenshow ?thesis by (rule rev_finite_subset) auto qed
lemma finite_not_eq_zero_sumI: fixes f g :: "'a::monoid_add \ 'b::semiring_0" assumes"finite {a. f a \ 0}" (is "finite ?F") assumes"finite {b. g b \ 0}" (is "finite ?G") shows"finite {a + b | a b. f a \ 0 \ g b \ 0}" (is "finite ?FG") proof - from assms have"finite (?F \ ?G)" by (simp add: finite_cartesian_product_iff) thenhave"finite (case_prod plus ` (?F \ ?G))" by (rule finite_imageI) alsohave"case_prod plus ` (?F \ ?G) = ?FG" by auto finallyshow ?thesis by simp qed
lemma finite_mult_not_eq_zero_sumI: fixes f g :: "'a::monoid_add \ 'b::semiring_0" assumes"finite {a. f a \ 0}" assumes"finite {b. g b \ 0}" shows"finite {a + b | a b. f a * g b \ 0}" proof - from assms have"finite {a + b | a b. f a \ 0 \ g b \ 0}" by (rule finite_not_eq_zero_sumI) thenshow ?thesis by (rule rev_finite_subset) (auto dest: mult_not_zero) qed
lemma finite_Sum_any_not_eq_zero_weakenI: assumes"finite {a. \b. f a b \ 0}" shows"finite {a. Sum_any (f a) \ 0}" proof - have"{a. Sum_any (f a) \ 0} \ {a. \b. f a b \ 0}" by (auto elim: Sum_any.not_neutral_obtains_not_neutral) thenshow ?thesis using assms by (rule finite_subset) qed
context zero begin
definition"when" :: "'a \ bool \ 'a" (infixl \when\ 20) where "(a when P) = (if P then a else 0)"
text\<open> Case distinctions always complicate matters, particularly when
nested. The @{const "when"} operation allows to minimise these if @{term 0} is the false-case valueand makes proof obligations
much more readable. \<close>
lemma"when" [simp]: "P \ (a when P) = a" "\ P \ (a when P) = 0" by (simp_all add: when_def)
lemma when_simps [simp]: "(a when True) = a" "(a when False) = 0" by simp_all
lemma when_cong: assumes"P \ Q" and"Q \ a = b" shows"(a when P) = (b when Q)" using assms by (simp add: when_def)
lemma zero_when [simp]: "(0 when P) = 0" by (simp add: when_def)
lemma when_when: "(a when P when Q) = (a when P \ Q)" by (cases Q) simp_all
lemma when_commute: "(a when Q when P) = (a when P when Q)" by (simp add: when_when conj_commute)
lemma when_neq_zero [simp]: "(a when P) \ 0 \ P \ a \ 0" by (cases P) simp_all
end
context monoid_add begin
lemma when_add_distrib: "(a + b when P) = (a when P) + (b when P)" by (simp add: when_def)
end
context semiring_1 begin
lemma zero_power_eq: "0 ^ n = (1 when n = 0)" by (simp add: power_0_left)
end
context comm_monoid_add begin
lemma Sum_any_when_equal [simp]: "(\a. (f a when a = b)) = f b" by (simp add: when_def)
lemma Sum_any_when_equal' [simp]: "(\a. (f a when b = a)) = f b" by (simp add: when_def)
lemma Sum_any_when_independent: "(\a. g a when P) = ((\a. g a) when P)" by (cases P) simp_all
lemma Sum_any_when_dependent_prod_right: "(\(a, b). g a when b = h a) = (\a. g a)" proof - have"inj_on (\a. (a, h a)) {a. g a \ 0}" by (rule inj_onI) auto thenshow ?thesis unfolding Sum_any.expand_set by (rule sum.reindex_cong) auto qed
lemma Sum_any_when_dependent_prod_left: "(\(a, b). g b when a = h b) = (\b. g b)" proof - have"(\(a, b). g b when a = h b) = (\(b, a). g b when a = h b)" by (rule Sum_any.reindex_cong [of prod.swap]) (simp_all add: fun_eq_iff) thenshow ?thesis by (simp add: Sum_any_when_dependent_prod_right) qed
end
context cancel_comm_monoid_add begin
lemma when_diff_distrib: "(a - b when P) = (a when P) - (b when P)" by (simp add: when_def)
end
context group_add begin
lemma when_uminus_distrib: "(- a when P) = - (a when P)" by (simp add: when_def)
end
context mult_zero begin
lemma mult_when: "a * (b when P) = (a * b when P)" by (cases P) simp_all
lemma when_mult: "(a when P) * b = (a * b when P)" by (cases P) simp_all
end
subsection \<open>Type definition\<close>
text\<open>
The following type is of central importance: \<close>
typedef (overloaded) ('a, 'b) poly_mapping (\<open>(_ \<Rightarrow>\<^sub>0 /_)\<close> [1, 0] 0) = "{f :: 'a \ 'b::zero. finite {x. f x \ 0}}" morphisms lookup Abs_poly_mapping using not_finite_existsD by force
lemma lookup_Abs_poly_mapping [simp]: "finite {x. f x \ 0} \ lookup (Abs_poly_mapping f) = f" using Abs_poly_mapping_inverse [of f] by simp
lemma finite_lookup [simp]: "finite {k. lookup f k \ 0}" using poly_mapping.lookup [of f] by simp
lemma finite_lookup_nat [simp]: fixes f :: "'a \\<^sub>0 nat" shows"finite {k. 0 < lookup f k}" using poly_mapping.lookup [of f] by simp
lemma poly_mapping_eqI: assumes"\k. lookup f k = lookup g k" shows"f = g" using assms unfolding poly_mapping.lookup_inject [symmetric] by blast
lemma poly_mapping_eq_iff: "a = b \ lookup a = lookup b" by auto
text\<open>
We model the universe of functions being \emph{almost everywhere zero} by means of a separate type @{typ"('a, 'b) poly_mapping"}. For convenience we provide a suggestive infixsyntax which is a variant of the usual function space syntax. Conversion between both types
happens through the morphisms \begin{quote}
@{term_type lookup} \end{quote} \begin{quote}
@{term_type Abs_poly_mapping} \end{quote}
satisfying \begin{quote}
@{thm lookup_inverse} \end{quote} \begin{quote}
@{thm lookup_Abs_poly_mapping} \end{quote}
Luckily, we have rarely to deal with those low-level morphisms explicitly
but rely on Isabelle's \emph{lifting} package with its method \transfer\ and its specification tool \<open>lift_definition\<close>. \<close>
setup_lifting type_definition_poly_mapping code_datatype Abs_poly_mapping\<comment>\<open>FIXME? workaround for preventing \<open>code_abstype\<close> setup\<close>
text\<open>
@{typ"'a \\<^sub>0 'b"} serves distinctive purposes: \begin{enumerate} \item A clever nesting as @{typ "(nat \<Rightarrow>\<^sub>0 nat) \<Rightarrow>\<^sub>0 'a"}
later intheory\<open>MPoly\<close> gives a suitable
representation type for polynomials \emph{almost for free}:
Interpreting @{typ"nat \\<^sub>0 nat"} as a mapping from variable identifiers to exponents yields monomials, and the whole type maps monomials to coefficients. Lets call this the \emph{ultimate interpretation}. \item A further more specialised type isomorphic to @{typ "nat \<Rightarrow>\<^sub>0 'a"} is apt to direct implementation using code generation \<^cite>\<open>"Haftmann-Nipkow:2010:code"\<close>. \end{enumerate} Note that despite the names \emph{mapping} and \emph{lookup} suggest something
implementation-near, it is best to keep @{typ"'a \\<^sub>0 'b"} as an abstract \emph{algebraic} type
providing operations like \emph{addition}, \emph{multiplication} without any notion
of key-order, data structures etc. This implementations-specific notions are
easily introduced later for particular implementations but do not provide any
gain for specifying logical properties of polynomials. \<close>
subsection \<open>Additive structure\<close>
text\<open>
The additive structure covers the usual operations \<open>0\<close>, \<open>+\<close> and
(unary and binary) \<open>-\<close>. Recalling the ultimate interpretation, it is obvious that these have just lift the corresponding operations on values to mappings.
Isabelle has a rich hierarchy of algebraic type classes, andin such situations
of pointwise lifting a typical pattern istohave instantiations for a considerable
number of type classes.
The operations themselves are specified using\<open>lift_definition\<close>, where
the proofs of the \emph{almost everywhere zero} property can be significantly involved.
The @{const lookup} operation is supposed to be usable explicitly (unless in
other situations where the morphisms between types are somehow internal to the \emph{lifting} package). Hence it is good style to provide explicit rewrite
rules how @{const lookup} acts on operations immediately. \<close>
instantiation poly_mapping :: (type, zero) zero begin
lift_definition zero_poly_mapping :: "'a \\<^sub>0 'b" is"\k. 0" by simp
lemma lookup_zero [simp]: "lookup 0 k = 0" by transfer rule
instantiation poly_mapping :: (type, monoid_add) monoid_add begin
lift_definition plus_poly_mapping :: "('a \\<^sub>0 'b) \ ('a \\<^sub>0 'b) \ 'a \\<^sub>0 'b" is"\f1 f2 k. f1 k + f2 k" proof - fix f1 f2 :: "'a \ 'b" assume"finite {k. f1 k \ 0}" and"finite {k. f2 k \ 0}" thenhave"finite ({k. f1 k \ 0} \ {k. f2 k \ 0})" by auto moreoverhave"{x. f1 x + f2 x \ 0} \ {k. f1 k \ 0} \ {k. f2 k \ 0}" by auto ultimatelyshow"finite {x. f1 x + f2 x \ 0}" by (blast intro: finite_subset) qed
instance by intro_classes (transfer, simp add: fun_eq_iff ac_simps)+
end
lemma lookup_add: "lookup (f + g) k = lookup f k + lookup g k" by (simp add: plus_poly_mapping.rep_eq)
instantiation poly_mapping :: (type, cancel_comm_monoid_add) cancel_comm_monoid_add begin
lift_definition minus_poly_mapping :: "('a \\<^sub>0 'b) \ ('a \\<^sub>0 'b) \ 'a \\<^sub>0 'b" is"\f1 f2 k. f1 k - f2 k" proof - fix f1 f2 :: "'a \ 'b" assume"finite {k. f1 k \ 0}" and"finite {k. f2 k \ 0}" thenhave"finite ({k. f1 k \ 0} \ {k. f2 k \ 0})" by auto moreoverhave"{x. f1 x - f2 x \ 0} \ {k. f1 k \ 0} \ {k. f2 k \ 0}" by auto ultimatelyshow"finite {x. f1 x - f2 x \ 0}" by (blast intro: finite_subset) qed
instance by intro_classes (transfer, simp add: fun_eq_iff diff_diff_add)+
end
instantiation poly_mapping :: (type, ab_group_add) ab_group_add begin
lift_definition uminus_poly_mapping :: "('a \\<^sub>0 'b) \ 'a \\<^sub>0 'b" is uminus by simp
instance by intro_classes (transfer, simp add: fun_eq_iff ac_simps)+
end
lemma lookup_uminus [simp]: "lookup (- f) k = - lookup f k" by transfer simp
lemma lookup_minus: "lookup (f - g) k = lookup f k - lookup g k" by transfer rule
definition prod_fun :: "('a \ 'b) \ ('a \ 'b) \ 'a::monoid_add \ 'b::semiring_0" where "prod_fun f1 f2 k = (\l. f1 l * (\q. (f2 q when k = l + q)))"
lemma prod_fun_unfold_prod: fixes f g :: "'a :: monoid_add \ 'b::semiring_0" assumes fin_f: "finite {a. f a \ 0}" assumes fin_g: "finite {b. g b \ 0}" shows"prod_fun f g k = (\(a, b). f a * g b when k = a + b)" proof - let ?C = "{a. f a \ 0} \ {b. g b \ 0}" from fin_f fin_g have"finite ?C"by blast moreover have"{a. \b. (f a * g b when k = a + b) \ 0} \
{b. \<exists>a. (f a * g b when k = a + b) \<noteq> 0} \<subseteq> {a. f a \<noteq> 0} \<times> {b. g b \<noteq> 0}" by auto ultimatelyshow ?thesis using fin_g by (auto simp: prod_fun_def
Sum_any.cartesian_product [of "{a. f a \ 0} \ {b. g b \ 0}"] Sum_any_right_distrib mult_when) qed
lemma finite_prod_fun: fixes f1 f2 :: "'a :: monoid_add \ 'b :: semiring_0" assumes fin1: "finite {l. f1 l \ 0}" and fin2: "finite {q. f2 q \ 0}" shows"finite {k. prod_fun f1 f2 k \ 0}" proof - have *: "finite {k. (\l. f1 l \ 0 \ (\q. f2 q \ 0 \ k = l + q))}" using assms by simp have aux: "sum f2 {q. f2 q \ 0 \ k = l + q} = (\q. (f2 q when k = l + q))" for k l proof - have"{q. (f2 q when k = l + q) \ 0} \ {q. f2 q \ 0 \ k = l + q}" by auto with fin2 show ?thesis by (simp add: Sum_any.expand_superset [of "{q. f2 q \ 0 \ k = l + q}"]) qed have"{k. (\l. f1 l * sum f2 {q. f2 q \ 0 \ k = l + q}) \ 0} \<subseteq> {k. (\<exists>l. f1 l * sum f2 {q. f2 q \<noteq> 0 \<and> k = l + q} \<noteq> 0)}" by (auto elim!: Sum_any.not_neutral_obtains_not_neutral) alsohave"\ \ {k. (\l. f1 l \ 0 \ sum f2 {q. f2 q \ 0 \ k = l + q} \ 0)}" by (auto dest: mult_not_zero) alsohave"\ \ {k. (\l. f1 l \ 0 \ (\q. f2 q \ 0 \ k = l + q))}" by (auto elim!: sum.not_neutral_contains_not_neutral) finallyhave"finite {k. (\l. f1 l * sum f2 {q. f2 q \ 0 \ k = l + q}) \ 0}" using * by (rule finite_subset) with aux have"finite {k. (\l. f1 l * (\q. (f2 q when k = l + q))) \ 0}" by simp with fin2 show ?thesis by (simp add: prod_fun_def) qed
instantiation poly_mapping :: (monoid_add, semiring_0) semiring_0 begin
lift_definition times_poly_mapping :: "('a \\<^sub>0 'b) \ ('a \\<^sub>0 'b) \ 'a \\<^sub>0 'b" is prod_fun by(rule finite_prod_fun)
instance proof fix a b c :: "'a \\<^sub>0 'b" show"a * b * c = a * (b * c)" proof transfer fix f g h :: "'a \ 'b" assume fin_f: "finite {a. f a \ 0}" (is "finite ?F") assume fin_g: "finite {b. g b \ 0}" (is "finite ?G") assume fin_h: "finite {c. h c \ 0}" (is "finite ?H") from fin_f fin_g have fin_fg: "finite {(a, b). f a * g b \ 0}" (is "finite ?FG") by (rule finite_mult_not_eq_zero_prodI) from fin_g fin_h have fin_gh: "finite {(b, c). g b * h c \ 0}" (is "finite ?GH") by (rule finite_mult_not_eq_zero_prodI) from fin_f fin_g have fin_fg': "finite {a + b | a b. f a * g b \ 0}" (is "finite ?FG'") by (rule finite_mult_not_eq_zero_sumI) thenhave fin_fg'': "finite {d. (\(a, b). f a * g b when d = a + b) \ 0}" by (auto intro: finite_Sum_any_not_eq_zero_weakenI) from fin_g fin_h have fin_gh': "finite {b + c | b c. g b * h c \ 0}" (is "finite ?GH'") by (rule finite_mult_not_eq_zero_sumI) thenhave fin_gh'': "finite {d. (\(b, c). g b * h c when d = b + c) \ 0}" by (auto intro: finite_Sum_any_not_eq_zero_weakenI) show"prod_fun (prod_fun f g) h = prod_fun f (prod_fun g h)" (is"?lhs = ?rhs") proof fix k from fin_f fin_g fin_h fin_fg'' have"?lhs k = (\(ab, c). (\(a, b). f a * g b when ab = a + b) * h c when k = ab + c)" by (simp add: prod_fun_unfold_prod) alsohave"\ = (\(ab, c). (\(a, b). f a * g b * h c when k = ab + c when ab = a + b))" using fin_fg apply (simp add: Sum_any_left_distrib split_def flip: Sum_any_when_independent) apply (simp add: when_when when_mult mult_when conj_commute) done alsohave"\ = (\(ab, c, a, b). f a * g b * h c when k = ab + c when ab = a + b)" apply (subst Sum_any.cartesian_product2 [of "(?FG' \ ?H) \ ?FG"]) apply (auto simp: finite_cartesian_product_iff fin_fg fin_fg' fin_h dest: mult_not_zero) done alsohave"\ = (\(ab, c, a, b). f a * g b * h c when k = a + b + c when ab = a + b)" by (rule Sum_any.cong) (simp add: split_def when_def) alsohave"\ = (\(ab, cab). (case cab of (c, a, b) \ f a * g b * h c when k = a + b + c)
when ab = (case cab of (c, a, b) \<Rightarrow> a + b))" by (simp add: split_def) alsohave"\ = (\(c, a, b). f a * g b * h c when k = a + b + c)" by (simp add: Sum_any_when_dependent_prod_left) alsohave"\ = (\(bc, cab). (case cab of (c, a, b) \ f a * g b * h c when k = a + b + c)
when bc = (case cab of (c, a, b) \<Rightarrow> b + c))" by (simp add: Sum_any_when_dependent_prod_left) alsohave"\ = (\(bc, c, a, b). f a * g b * h c when k = a + b + c when bc = b + c)" by (simp add: split_def) alsohave"\ = (\(bc, c, a, b). f a * g b * h c when bc = b + c when k = a + bc)" by (rule Sum_any.cong) (simp add: split_def when_def ac_simps) alsohave"\ = (\(a, bc, b, c). f a * g b * h c when bc = b + c when k = a + bc)" proof - have"bij (\(a, d, b, c). (d, c, a, b))" by (auto intro!: bijI injI surjI [of _ "\(d, c, a, b). (a, d, b, c)"] simp add: split_def) thenshow ?thesis by (rule Sum_any.reindex_cong) auto qed alsohave"\ = (\(a, bc). (\(b, c). f a * g b * h c when bc = b + c when k = a + bc))" apply (subst Sum_any.cartesian_product2 [of "(?F \ ?GH') \ ?GH"]) apply (auto simp: finite_cartesian_product_iff fin_f fin_gh fin_gh' ac_simps dest: mult_not_zero) done alsohave"\ = (\(a, bc). f a * (\(b, c). g b * h c when bc = b + c) when k = a + bc)" apply (subst Sum_any_right_distrib) using fin_gh apply (simp add: split_def) apply (subst Sum_any_when_independent [symmetric]) apply (simp add: when_when when_mult mult_when split_def ac_simps) done alsofrom fin_f fin_g fin_h fin_gh'' have"\ = ?rhs k" by (simp add: prod_fun_unfold_prod) finallyshow"?lhs k = ?rhs k" . qed qed show"(a + b) * c = a * c + b * c" proof transfer fix f g h :: "'a \ 'b" assume fin_f: "finite {k. f k \ 0}" assume fin_g: "finite {k. g k \ 0}" assume fin_h: "finite {k. h k \ 0}" show"prod_fun (\k. f k + g k) h = (\k. prod_fun f h k + prod_fun g h k)" apply (rule ext) apply (simp add: prod_fun_def algebra_simps) by (simp add: Sum_any.distrib fin_f fin_g finite_mult_not_eq_zero_rightI) qed show"a * (b + c) = a * b + a * c" proof transfer fix f g h :: "'a \ 'b" assume fin_f: "finite {k. f k \ 0}" assume fin_g: "finite {k. g k \ 0}" assume fin_h: "finite {k. h k \ 0}" show"prod_fun f (\k. g k + h k) = (\k. prod_fun f g k + prod_fun f h k)" apply (rule ext) apply (auto simp: prod_fun_def Sum_any.distrib algebra_simps when_add_distrib fin_g fin_h) by (simp add: Sum_any.distrib fin_f finite_mult_not_eq_zero_rightI) qed show"0 * a = 0" by transfer (simp add: prod_fun_def [abs_def]) show"a * 0 = 0" by transfer (simp add: prod_fun_def [abs_def]) qed
end
lemma lookup_mult: "lookup (f * g) k = (\l. lookup f l * (\q. lookup g q when k = l + q))" by transfer (simp add: prod_fun_def)
instance poly_mapping :: (comm_monoid_add, comm_semiring_0) comm_semiring_0 proof fix a b c :: "'a \\<^sub>0 'b" show"a * b = b * a" proof transfer fix f g :: "'a \ 'b" assume fin_f: "finite {a. f a \ 0}" assume fin_g: "finite {b. g b \ 0}" show"prod_fun f g = prod_fun g f" proof fix k have fin1: "\l. finite {a. (f a when k = l + a) \ 0}" using fin_f by auto have fin2: "\l. finite {b. (g b when k = l + b) \ 0}" using fin_g by auto from fin_f fin_g have"finite {(a, b). f a \ 0 \ g b \ 0}" (is "finite ?AB") by simp have"(\a. \n. f a * (g n when k = a + n)) = (\a. \n. g a * (f n when k = a + n))" by (subst Sum_any.swap [OF \<open>finite ?AB\<close>]) (auto simp: mult_when ac_simps) thenshow"prod_fun f g k = prod_fun g f k" by (simp add: prod_fun_def Sum_any_right_distrib [OF fin2] Sum_any_right_distrib [OF fin1]) qed qed show"(a + b) * c = a * c + b * c" proof transfer fix f g h :: "'a \ 'b" assume fin_f: "finite {k. f k \ 0}" assume fin_g: "finite {k. g k \ 0}" assume fin_h: "finite {k. h k \ 0}" show"prod_fun (\k. f k + g k) h = (\k. prod_fun f h k + prod_fun g h k)" by (auto simp: prod_fun_def fun_eq_iff algebra_simps
Sum_any.distrib fin_f fin_g finite_mult_not_eq_zero_rightI) qed qed
instance poly_mapping :: (monoid_add, semiring_1) semiring_1 proof fix a :: "'a \\<^sub>0 'b" show"1 * a = a" by transfer (simp add: prod_fun_def [abs_def] when_mult) show"a * 1 = a" apply transfer apply (simp add: prod_fun_def [abs_def] Sum_any_right_distrib Sum_any_left_distrib mult_when) apply (subst when_commute) apply simp done qed
instance poly_mapping :: (comm_monoid_add, comm_semiring_1) comm_semiring_1 proof fix a :: "'a \\<^sub>0 'b" show"1 * a = a" by transfer (simp add: prod_fun_def [abs_def]) qed
lift_definition single :: "'a \ 'b \ 'a \\<^sub>0 'b::zero" is"\k v k'. (v when k = k')" by simp
lemma inj_single [iff]: "inj (single k)" proof (rule injI, transfer) fix k :: 'b and a b :: "'a::zero" assume"(\k'. a when k = k') = (\k'. b when k = k')" thenhave"(\k'. a when k = k') k = (\k'. b when k = k') k" by (rule arg_cong) thenshow"a = b"by simp qed
lemma lookup_single: "lookup (single k v) k' = (v when k = k')" by (simp add: single.rep_eq)
lemma lookup_single_eq [simp]: "lookup (single k v) k = v" by (simp add: single.rep_eq)
lemma lookup_single_not_eq: "k \ k' \ lookup (single k v) k' = 0" by (simp add: single.rep_eq)
lemma single_zero [simp]: "single k 0 = 0" by transfer simp
lemma single_one [simp]: "single 0 1 = 1" by transfer simp
lemma single_add: "single k (a + b) = single k a + single k b" by transfer (simp add: fun_eq_iff when_add_distrib)
lemma single_uminus: "single k (- a) = - single k a" by transfer (simp add: fun_eq_iff when_uminus_distrib)
lemma single_diff: "single k (a - b) = single k a - single k b" by transfer (simp add: fun_eq_iff when_diff_distrib)
lemma lookup_numeral: "lookup (numeral n) k = (numeral n when k = 0)" proof - have"lookup (numeral n) k = lookup (single 0 (numeral n)) k" by simp thenshow ?thesis unfolding lookup_single by simp qed
lemma lookup_of_nat: "lookup (of_nat n) k = (of_nat n when k = 0)" by (metis lookup_single lookup_single_not_eq single_of_nat)
lemma of_nat_single: "of_nat = single 0 \ of_nat" by (simp add: fun_eq_iff)
lemma mult_single: "single k a * single l b = single (k + l) (a * b)" proof transfer fix k l :: 'a and a b :: 'b show"prod_fun (\k'. a when k = k') (\k'. b when l = k') = (\k'. a * b when k + l = k')" proof fix k' have"prod_fun (\k'. a when k = k') (\k'. b when l = k') k' = (\n. a * b when l = n when k' = k + n)" by (simp add: prod_fun_def Sum_any_right_distrib mult_when when_mult) alsohave"\ = (\n. a * b when k' = k + n when l = n)" by (simp add: when_when conj_commute) alsohave"\ = (a * b when k' = k + l)" by simp alsohave"\ = (a * b when k + l = k')" by (simp add: when_def) finallyshow"prod_fun (\k'. a when k = k') (\k'. b when l = k') k' =
(\<lambda>k'. a * b when k + l = k') k'" . qed qed
lemma lookup_of_int: "lookup (of_int l) k = (of_int l when k = 0)" by (metis lookup_single_not_eq single.rep_eq single_of_int)
subsection \<open>Integral domains\<close>
instance poly_mapping :: ("{ordered_cancel_comm_monoid_add, linorder}", semiring_no_zero_divisors) semiring_no_zero_divisors text\<open>The @{class "linorder"} constraint is a pragmatic device for the proof --- maybe it can be dropped\<close> proof fix f g :: "'a \\<^sub>0 'b" assume"f \ 0" and "g \ 0" thenshow"f * g \ 0" proof transfer fix f g :: "'a \ 'b"
define F where"F = {a. f a \ 0}" moreover define G where"G = {a. g a \ 0}" ultimatelyhave [simp]: "\a. f a \ 0 \ a \ F" "\b. g b \ 0 \ b \ G" by simp_all assume"finite {a. f a \ 0}" thenhave [simp]: "finite F" by simp assume"finite {a. g a \ 0}" thenhave [simp]: "finite G" by simp assume"f \ (\a. 0)" thenobtain a where"f a \ 0" by (auto simp: fun_eq_iff) assume"g \ (\b. 0)" thenobtain b where"g b \ 0" by (auto simp: fun_eq_iff) from\<open>f a \<noteq> 0\<close> and \<open>g b \<noteq> 0\<close> have "F \<noteq> {}" and "G \<noteq> {}" by auto note Max_F = \<open>finite F\<close> \<open>F \<noteq> {}\<close> note Max_G = \<open>finite G\<close> \<open>G \<noteq> {}\<close> from Max_F and Max_G have [simp]: "Max F \ F" "Max G \ G" by auto from Max_F Max_G have [dest!]: "\a. a \ F \ a \ Max F" "\b. b \ G \ b \ Max G" by auto
define q where"q = Max F + Max G" have"(\(a, b). f a * g b when q = a + b) =
(\<Sum>(a, b). f a * g b when q = a + b when a \<in> F \<and> b \<in> G)" by (rule Sum_any.cong) (auto simp: split_def when_def q_def intro: ccontr) alsohave"\ =
(\<Sum>(a, b). f a * g b when (Max F, Max G) = (a, b))" proof (rule Sum_any.cong) fix ab :: "'a \ 'a" obtain a b where [simp]: "ab = (a, b)" by (cases ab) simp_all have [dest!]: "a \ Max F \ Max F \ a \ a < Max F" "b \ Max G \ Max G \ b \ b < Max G" by auto show"(case ab of (a, b) \ f a * g b when q = a + b when a \ F \ b \ G) =
(case ab of (a, b) \<Rightarrow> f a * g b when (Max F, Max G) = (a, b))" by (auto simp: split_def when_def q_def dest: add_strict_mono [of a "Max F" b "Max G"]) qed alsohave"\ = (\ab. (case ab of (a, b) \ f a * g b) when
(Max F, Max G) = ab)" unfolding split_def when_def by auto alsohave"\ \ 0" by simp finallyhave"prod_fun f g q \ 0" by (simp add: prod_fun_unfold_prod) thenshow"prod_fun f g \ (\k. 0)" by (auto simp: fun_eq_iff) qed qed
lift_definition less_eq_poly_mapping :: "('a \\<^sub>0 'b) \ ('a \\<^sub>0 'b) \ bool" is"\f g. less_fun f g \ f = g"
.
instanceproof (rule linorder.intro_of_class) show"class.linorder (less_eq :: (_ \\<^sub>0 _) \ _) less" proof (rule linorder_strictI, rule order_strictI) fix f g h :: "'a \\<^sub>0 'b" show"f \ g \ f < g \ f = g" by transfer (rule refl) show"\ f < f" by transfer (rule less_fun_irrefl) show"f < g \ f = g \ g < f" proof transfer fix f g :: "'a \ 'b" assume"finite {k. f k \ 0}" and "finite {k. g k \ 0}" thenhave"finite ({k. f k \ 0} \ {k. g k \ 0})" by simp moreoverhave"{k. f k \ g k} \ {k. f k \ 0} \ {k. g k \ 0}" by auto ultimatelyhave"finite {k. f k \ g k}" by (rule rev_finite_subset) thenshow"less_fun f g \ f = g \ less_fun g f" by (rule less_fun_trichotomy) qed assume"f < g"thenshow"\ g < f" by transfer (rule less_fun_asym) note\<open>f < g\<close> moreover assume "g < h" ultimatelyshow"f < h" by transfer (rule less_fun_trans) qed qed
end
instance poly_mapping :: (linorder, "{ordered_comm_monoid_add, ordered_ab_semigroup_add_imp_le, linorder}") ordered_ab_semigroup_add proof (intro_classes, transfer) fix f g h :: "'a \ 'b" assume *: "less_fun f g \ f = g" have"less_fun (\k. h k + f k) (\k. h k + g k)" if "less_fun f g" by (metis (no_types, lifting) less_fun_def add_strict_left_mono that) with * show"less_fun (\k. h k + f k) (\k. h k + g k) \ (\k. h k + f k) = (\k. h k + g k)" by (auto simp: fun_eq_iff) qed
text\<open> For pragmatism we leave out the final elements in the hierarchy:
@{class linordered_ring}, @{class linordered_ring_strict}, @{class linordered_idom};
remember that the order instanceis a mere technical device, not a deeper algebraic
property. \<close>
lift_definition keys :: "('a \\<^sub>0 'b::zero) \ 'a set" is"\f. {k. f k \ 0}" .
lift_definition range :: "('a \\<^sub>0 'b::zero) \ 'b set" is"\f :: 'a \ 'b. Set.range f - {0}" .
lemma finite_keys [simp]: "finite (keys f)" by transfer
lemma not_in_keys_iff_lookup_eq_zero: "k \ keys f \ lookup f k = 0" by transfer simp
lemma lookup_not_eq_zero_eq_in_keys: "lookup f k \ 0 \ k \ keys f" by transfer simp
lemma lookup_eq_zero_in_keys_contradict [dest]: "lookup f k = 0 \ \ k \ keys f" by (simp add: not_in_keys_iff_lookup_eq_zero)
lemma finite_range [simp]: "finite (Poly_Mapping.range p)" proof transfer fix f :: "'b \ 'a" assume *: "finite {x. f x \ 0}" have"Set.range f - {0} \ f ` {x. f x \ 0}" by auto thus"finite (Set.range f - {0})" using"*" finite_surj by blast qed
lemma in_keys_lookup_in_range [simp]: "k \ keys f \ lookup f k \ range f" by transfer simp
lemma in_keys_iff: "x \ (keys s) = (lookup s x \ 0)" by (simp add: lookup_not_eq_zero_eq_in_keys)
lemma keys_zero [simp]: "keys 0 = {}" by transfer simp
lemma range_zero [simp]: "range 0 = {}" by transfer auto
lemma keys_add: "keys (f + g) \ keys f \ keys g" by transfer auto
lemma keys_one [simp]: "keys 1 = {0}" by transfer simp
lemma range_one [simp]: "range 1 = {1}" by transfer (auto simp: when_def)
lemma keys_single [simp]: "keys (single k v) = (if v = 0 then {} else {k})" by transfer simp
lemma range_single [simp]: "range (single k v) = (if v = 0 then {} else {v})" by transfer (auto simp: when_def)
lemma keys_mult: "keys (f * g) \ {a + b | a b. a \ keys f \ b \ keys g}" apply transfer apply (force simp: prod_fun_def dest!: mult_not_zero elim!: Sum_any.not_neutral_obtains_not_neutral) done
lemma setsum_keys_plus_distrib: assumes hom_0: "\k. f k 0 = 0" and hom_plus: "\k. k \ Poly_Mapping.keys p \ Poly_Mapping.keys q \ f k (Poly_Mapping.lookup p k + Poly_Mapping.lookup q k) = f k (Poly_Mapping.lookup p k) + f k (Poly_Mapping.lookup q k)" shows "(\k\Poly_Mapping.keys (p + q). f k (Poly_Mapping.lookup (p + q) k)) =
(\<Sum>k\<in>Poly_Mapping.keys p. f k (Poly_Mapping.lookup p k)) +
(\<Sum>k\<in>Poly_Mapping.keys q. f k (Poly_Mapping.lookup q k))"
(is"?lhs = ?p + ?q") proof - let ?A = "Poly_Mapping.keys p \ Poly_Mapping.keys q" have"?lhs = (\k\?A. f k (Poly_Mapping.lookup p k + Poly_Mapping.lookup q k))" by(intro sum.mono_neutral_cong_left) (auto simp: sum.mono_neutral_cong_left hom_0 in_keys_iff lookup_add) alsohave"\ = (\k\?A. f k (Poly_Mapping.lookup p k) + f k (Poly_Mapping.lookup q k))" by(rule sum.cong)(simp_all add: hom_plus) alsohave"\ = (\k\?A. f k (Poly_Mapping.lookup p k)) + (\k\?A. f k (Poly_Mapping.lookup q k))"
(is"_ = ?p' + ?q'") by(simp add: sum.distrib) alsohave"?p' = ?p" by (simp add: hom_0 in_keys_iff sum.mono_neutral_cong_right) alsohave"?q' = ?q" by (simp add: hom_0 in_keys_iff sum.mono_neutral_cong_right) finallyshow ?thesis . qed
subsection \<open>Degree\<close>
definition degree :: "(nat \\<^sub>0 'a::zero) \ nat" where "degree f = Max (insert 0 (Suc ` keys f))"
lemma degree_zero [simp]: "degree 0 = 0" unfolding degree_def by transfer simp
lemma degree_one [simp]: "degree 1 = 1" unfolding degree_def by transfer simp
lemma degree_single_zero [simp]: "degree (single k 0) = 0" unfolding degree_def by transfer simp
lemma degree_single_not_zero [simp]: "v \ 0 \ degree (single k v) = Suc k" unfolding degree_def by transfer simp
lemma degree_zero_iff [simp]: "degree f = 0 \ f = 0" unfolding degree_def proof transfer fix f :: "nat \ 'a" assume"finite {n. f n \ 0}" thenhave fin: "finite (insert 0 (Suc ` {n. f n \ 0}))" by auto show"Max (insert 0 (Suc ` {n. f n \ 0})) = 0 \ f = (\n. 0)" (is "?P \ ?Q") proof assume ?P have"{n. f n \ 0} = {}" proof (rule ccontr) assume"{n. f n \ 0} \ {}" thenobtain n where"n \ {n. f n \ 0}" by blast thenhave"{n. f n \ 0} = insert n {n. f n \ 0}" by auto thenhave"Suc ` {n. f n \ 0} = insert (Suc n) (Suc ` {n. f n \ 0})" by auto with\<open>?P\<close> have "Max (insert 0 (insert (Suc n) (Suc ` {n. f n \<noteq> 0}))) = 0" by simp thenhave"Max (insert (Suc n) (insert 0 (Suc ` {n. f n \ 0}))) = 0" by (simp add: insert_commute) with fin have"max (Suc n) (Max (insert 0 (Suc ` {n. f n \ 0}))) = 0" by simp thenshow False by simp qed thenshow ?Q by (simp add: fun_eq_iff) next assume ?Q thenshow ?P by simp qed qed
lemma degree_greater_zero_in_keys: assumes"0 < degree f" shows"degree f - 1 \ keys f" proof - from assms have"keys f \ {}" by (auto simp: degree_def) thenshow ?thesis unfolding degree_def by (simp add: mono_Max_commute [symmetric] mono_Suc) qed
lemma in_keys_less_degree: "n \ keys f \ n < degree f" unfolding degree_def by transfer (auto simp: Max_gr_iff)
lemma beyond_degree_lookup_zero: "degree f \ n \ lookup f n = 0" unfolding degree_def by transfer auto
lemma degree_add: "degree (f + g) \ max (degree f) (Poly_Mapping.degree g)" unfolding degree_def proof transfer fix f g :: "nat \ 'a" assume f: "finite {x. f x \ 0}" assume g: "finite {x. g x \ 0}" let ?f = "Max (insert 0 (Suc ` {k. f k \ 0}))" let ?g = "Max (insert 0 (Suc ` {k. g k \ 0}))" have"Max (insert 0 (Suc ` {k. f k + g k \ 0})) \ Max (insert 0 (Suc ` ({k. f k \ 0} \ {k. g k \ 0})))" by (rule Max.subset_imp) (insert f g, auto) alsohave"\ = max ?f ?g" using f g by (simp_all add: image_Un Max_Un [symmetric]) finallyshow"Max (insert 0 (Suc ` {k. f k + g k \ 0})) \<le> max (Max (insert 0 (Suc ` {k. f k \<noteq> 0}))) (Max (insert 0 (Suc ` {k. g k \<noteq> 0})))"
. qed
lemma sorted_list_of_set_keys: "sorted_list_of_set (keys f) = filter (\k. k \ keys f) [0.. proof - have"keys f = set ?r" by (auto dest: in_keys_less_degree) moreoverhave"sorted_list_of_set (set ?r) = ?r" unfolding sorted_list_of_set_sort_remdups by (simp add: remdups_filter filter_sort [symmetric]) ultimatelyshow ?thesis by simp qed
subsection \<open>Inductive structure\<close>
lift_definition update :: "'a \ 'b \ ('a \\<^sub>0 'b::zero) \ 'a \\<^sub>0 'b" is"\k v f. f(k := v)" proof - fix f :: "'a \ 'b" and k' v assume"finite {k. f k \ 0}" thenhave"finite (insert k' {k. f k \ 0})" by simp thenshow"finite {k. (f(k' := v)) k \ 0}" by (rule rev_finite_subset) auto qed
lemma update_induct [case_names const update]: assumes const': "P 0" assumes update': "\f a b. a \ keys f \ b \ 0 \ P f \ P (update a b f)" shows"P f" proof - obtain g where"f = Abs_poly_mapping g"and"finite {a. g a \ 0}" by (cases f) simp_all
define Q where"Q g = P (Abs_poly_mapping g)"for g from\<open>finite {a. g a \<noteq> 0}\<close> have "Q g" proof (induct g rule: finite_update_induct) case const with const' Q_def show ?case by simp next case (update a b g) from\<open>finite {a. g a \<noteq> 0}\<close> \<open>g a = 0\<close> have "a \<notin> keys (Abs_poly_mapping g)" by (simp add: Abs_poly_mapping_inverse keys.rep_eq) moreovernote\<open>b \<noteq> 0\<close> moreoverfrom\<open>Q g\<close> have "P (Abs_poly_mapping g)" by (simp add: Q_def) ultimatelyhave"P (update a b (Abs_poly_mapping g))" by (rule update') alsofrom\<open>finite {a. g a \<noteq> 0}\<close> have"update a b (Abs_poly_mapping g) = Abs_poly_mapping (g(a := b))" by (simp add: update.abs_eq eq_onp_same_args) finallyshow ?case by (simp add: Q_def fun_upd_def) qed thenshow ?thesis by (simp add: Q_def \<open>f = Abs_poly_mapping g\<close>) qed
lemma lookup_update: "lookup (update k v f) k' = (if k = k' then v else lookup f k')" by transfer simp
lemma keys_update: "keys (update k v f) = (if v = 0 then keys f - {k} else insert k (keys f))" by transfer auto
lift_definition map :: "('b::zero \ 'c::zero) \<Rightarrow> ('a \<Rightarrow>\<^sub>0 'b) \<Rightarrow> ('a \<Rightarrow>\<^sub>0 'c::zero)" is"\g f k. g (f k) when f k \ 0" by simp
context fixes f :: "'b \ 'a" assumes inj_f: "inj f" begin
lift_definition map_key :: "('a \\<^sub>0 'c::zero) \ 'b \\<^sub>0 'c" is"\p. p \ f" proof - fix g :: "'c \ 'd" and p :: "'a \ 'c" assume"finite {x. p x \ 0}" hence"finite (f ` {y. p (f y) \ 0})" by (simp add: rev_finite_subset subset_eq) thus"finite {x. (p \ f) x \ 0}" unfolding o_def by (metis finite_imageD injD inj_f inj_on_def) qed
end
lemma map_key_compose: assumes [transfer_rule]: "inj f""inj g" shows"map_key f (map_key g p) = map_key (g \ f) p" proof - from assms have [transfer_rule]: "inj (g \ f)" by(simp add: inj_compose) show ?thesis by transfer(simp add: o_assoc) qed
lemma map_key_id: "map_key (\x. x) p = p" proof - have [transfer_rule]: "inj (\x. x)" by simp show ?thesis by transfer(simp add: o_def) qed
context fixes f :: "'a \ 'b" assumes inj_f [transfer_rule]: "inj f" begin
lemma map_key_map: "map_key f (map g p) = map g (map_key f p)" by transfer (simp add: fun_eq_iff)
lemma map_key_plus: "map_key f (p + q) = map_key f p + map_key f q" by transfer (simp add: fun_eq_iff)
lemma keys_map_key: "keys (map_key f p) = f -` keys p" by transfer auto
lemma map_key_zero [simp]: "map_key f 0 = 0" by transfer (simp add: fun_eq_iff)
lemma map_key_single [simp]: "map_key f (single (f k) v) = single k v" by transfer (simp add: fun_eq_iff inj_onD [OF inj_f] when_def)
end
lemma mult_map_scale_conv_mult: "map ((*) s) p = single 0 s * p" proof(transfer fixing: s) fix p :: "'a \ 'b" assume *: "finite {x. p x \ 0}" have"prod_fun (\k'. s when 0 = k') p x = (\k. s * p k when p k \ 0) x" (is "?lhs = ?rhs") for x proof - have"?lhs = (\l :: 'a. if l = 0 then s * (\q. p q when x = q) else 0)" by (auto simp: prod_fun_def when_def intro: Sum_any.cong simp del: Sum_any.delta) alsohave"\ = ?rhs" by (simp add: when_def) finallyshow ?thesis . qed thenshow"(\k. s * p k when p k \ 0) = prod_fun (\k'. s when 0 = k') p" by(simp add: fun_eq_iff) qed
lemma map_single [simp]: "(c = 0 \ f 0 = 0) \ map f (single x c) = single x (f c)" by transfer(auto simp: fun_eq_iff when_def)
lemma map_eq_zero_iff: "map f p = 0 \ (\k \ keys p. f (lookup p k) = 0)" by transfer(auto simp: fun_eq_iff when_def)
subsection \<open>Canonical dense representation of @{typ "nat \<Rightarrow>\<^sub>0 'a"}\<close>
abbreviation no_trailing_zeros :: "'a :: zero list \ bool" where "no_trailing_zeros \ no_trailing ((=) 0)"
lift_definition "nth" :: "'a list \ (nat \\<^sub>0 'a::zero)" is"nth_default 0" by (fact finite_nth_default_neq_default)
text\<open>
The opposite direction is directly specified on (later)
type \<open>nat_mapping\<close>. \<close>
lemma nth_Nil [simp]: "nth [] = 0" by transfer (simp add: fun_eq_iff)
lemma nth_singleton [simp]: "nth [v] = single 0 v" proof (transfer, rule ext) fix n :: nat and v :: 'a show"nth_default 0 [v] n = (v when 0 = n)" by (auto simp: nth_default_def nth_append) qed
lemma nth_replicate [simp]: "nth (replicate n 0 @ [v]) = single n v" proof (transfer, rule ext) fix m n :: nat and v :: 'a show"nth_default 0 (replicate n 0 @ [v]) m = (v when n = m)" by (auto simp: nth_default_def nth_append) qed
lemma nth_strip_while [simp]: "nth (strip_while ((=) 0) xs) = nth xs" by transfer (fact nth_default_strip_while_dflt)
lemma nth_strip_while' [simp]: "nth (strip_while (\k. k = 0) xs) = nth xs" by (subst eq_commute) (fact nth_strip_while)
lemma keys_nth [simp]: "keys (nth xs) = fst ` {(n, v) \ set (enumerate 0 xs). v \ 0}" proof transfer fix xs :: "'a list" have"n \ fst ` {(n, v). (n, v) \ set (enumerate 0 xs) \ v \ 0}" if"nth_default 0 xs n \ 0" for n proof - from that have"n < length xs"and"xs ! n \ 0" by (auto simp: nth_default_def split: if_splits) thenhave"(n, xs ! n) \ {(n, v). (n, v) \ set (enumerate 0 xs) \ v \ 0}" (is "?x \ ?A") by (auto simp: in_set_conv_nth enumerate_eq_zip) thenhave"fst ?x \ fst ` ?A" by blast thenshow ?thesis by simp qed thenshow"{k. nth_default 0 xs k \ 0} = fst ` {(n, v). (n, v) \ set (enumerate 0 xs) \ v \ 0}" by (auto simp: in_enumerate_iff_nth_default_eq) qed
lemma range_nth [simp]: "range (nth xs) = set xs - {0}" by transfer simp
lemma degree_nth: "no_trailing_zeros xs \ degree (nth xs) = length xs" unfolding degree_def proof transfer fix xs :: "'a list" assume *: "no_trailing_zeros xs" let ?A = "{n. nth_default 0 xs n \ 0}" let ?f = "nth_default 0 xs" let ?bound = "Max (insert 0 (Suc ` {n. ?f n \ 0}))" show"?bound = length xs" proof (cases "xs = []") case False with * obtain n where n: "n < length xs""xs ! n \ 0" by (fastforce simp add: no_trailing_unfold last_conv_nth neq_Nil_conv) thenhave"?bound = Max (Suc ` {k. (k < length xs \ xs ! k \ (0::'a)) \ k < length xs})" by (subst Max_insert) (auto simp: nth_default_def) alsolet ?A = "{k. k < length xs \ xs ! k \ 0}" have"{k. (k < length xs \ xs ! k \ (0::'a)) \ k < length xs} = ?A" by auto alsohave"Max (Suc ` ?A) = Suc (Max ?A)"using n by (subst mono_Max_commute [where f = Suc, symmetric]) (auto simp: mono_Suc) also { have"Max ?A \ ?A" using n Max_in [of ?A] by fastforce hence"Suc (Max ?A) \ length xs" by simp moreoverfrom * False have"length xs - 1 \ ?A" by(auto simp: no_trailing_unfold last_conv_nth) hence"length xs - 1 \ Max ?A" using Max_ge[of ?A "length xs - 1"] by auto hence"length xs \ Suc (Max ?A)" by simp ultimatelyhave"Suc (Max ?A) = length xs"by simp } finallyshow ?thesis . qed simp qed
lemma nth_trailing_zeros [simp]: "nth (xs @ replicate n 0) = nth xs" by (simp add: nth.abs_eq)
lemma nth_idem: "nth (List.map (lookup f) [0.. unfolding degree_def by transfer
(auto simp: nth_default_def fun_eq_iff not_less)
lemma nth_idem_bound: assumes"degree f \ n" shows"nth (List.map (lookup f) [0.. proof - from assms obtain m where"n = degree f + m" by (blast dest: le_Suc_ex) thenhave"[0.. by (simp add: upt_add_eq_append [of 0]) moreoverhave"List.map (lookup f) [degree f.. by (rule replicate_eqI) (auto simp: beyond_degree_lookup_zero) ultimatelyshow ?thesis by (simp add: nth_idem) qed
subsection \<open>Canonical sparse representation of @{typ "'a \<Rightarrow>\<^sub>0 'b"}\<close>
lift_definition the_value :: "('a \ 'b) list \ 'a \\<^sub>0 'b::zero" is"\xs k. case map_of xs k of None \ 0 | Some v \ v" proof - fix xs :: "('a \ 'b) list" have fin: "finite {k. \v. map_of xs k = Some v}" using finite_dom_map_of [of xs] unfolding dom_def by auto thenshow"finite {k. (case map_of xs k of None \ 0 | Some v \ v) \ 0}" using fin by (simp split: option.split) qed
definition items :: "('a::linorder \\<^sub>0 'b::zero) \ ('a \ 'b) list" where "items f = List.map (\k. (k, lookup f k)) (sorted_list_of_set (keys f))"
text\<open> For the canonical sparse representation we provide both
directions of morphisms since the specification of
ordered association lists intheory\<open>OAList\<close>
will support arbitrary linear orders @{class linorder}
as keys, not just natural numbers @{typ nat}. \<close>
lemma the_value_items [simp]: "the_value (items f) = f" unfolding items_def by transfer (simp add: fun_eq_iff map_of_map_restrict restrict_map_def)
lemma lookup_the_value: "lookup (the_value xs) k = (case map_of xs k of None \ 0 | Some v \ v)" by (simp add: the_value.rep_eq)
lemma items_the_value: assumes"sorted (List.map fst xs)"and"distinct (List.map fst xs)"and"0 \ snd ` set xs" shows"items (the_value xs) = xs" proof - from assms have"sorted_list_of_set (set (List.map fst xs)) = List.map fst xs" unfolding sorted_list_of_set_sort_remdups by (simp add: distinct_remdups_id sort_key_id_if_sorted) moreoverfrom assms have"keys (the_value xs) = fst ` set xs" by transfer (auto simp: image_def split: option.split dest: set_map_of_compr) ultimatelyshow ?thesis unfolding items_def using assms by (auto simp: lookup_the_value intro: map_idI) qed
lemma the_value_Nil [simp]: "the_value [] = 0" by transfer (simp add: fun_eq_iff)
lemma the_value_Cons [simp]: "the_value (x # xs) = update (fst x) (snd x) (the_value xs)" by transfer (simp add: fun_eq_iff)
lemma items_one [simp]: "items 1 = [(0, 1)]" unfolding items_def by transfer simp
lemma items_single [simp]: "items (single k v) = (if v = 0 then [] else [(k, v)])" unfolding items_def by simp
lemma in_set_items_iff [simp]: "(k, v) \ set (items f) \ k \ keys f \ lookup f k = v" unfolding items_def by transfer auto
subsection \<open>Size estimation\<close>
context fixes f :: "'a \ nat" and g :: "'b :: zero \ nat" begin
definition poly_mapping_size :: "('a \\<^sub>0 'b) \ nat" where "poly_mapping_size m = g 0 + (\k \ keys m. Suc (f k + g (lookup m k)))"
lemma poly_mapping_size_0 [simp]: "poly_mapping_size 0 = g 0" by (simp add: poly_mapping_size_def)
lemma poly_mapping_size_single [simp]: "poly_mapping_size (single k v) = (if v = 0 then g 0 else g 0 + f k + g v + 1)" unfolding poly_mapping_size_def by transfer simp
lemma keys_less_poly_mapping_size: "k \ keys m \ f k + g (lookup m k) < poly_mapping_size m" unfolding poly_mapping_size_def proof transfer fix k :: 'a and m :: "'a \<Rightarrow> 'b" and f :: "'a \<Rightarrow> nat" and g let ?keys = "{k. m k \ 0}" assume *: "finite ?keys""k \ ?keys" thenhave"f k + g (m k) = (\k' \ ?keys. f k' + g (m k') when k' = k)" by (simp add: sum.delta when_def) alsohave"\ < (\k' \ ?keys. Suc (f k' + g (m k')))" using * by (intro sum_strict_mono) (auto simp: when_def) alsohave"\ \ g 0 + \" by simp finallyhave"f k + g (m k) < \" . thenshow"f k + g (m k) < g 0 + (\k | m k \ 0. Suc (f k + g (m k)))" by simp qed
lemma lookup_le_poly_mapping_size: "g (lookup m k) \ poly_mapping_size m" proof (cases "k \ keys m") case True with keys_less_poly_mapping_size [of k m] show ?thesis by simp next case False thenshow ?thesis by (simp add: Poly_Mapping.poly_mapping_size_def in_keys_iff) qed
lemma poly_mapping_size_estimation: "k \ keys m \ y \ f k + g (lookup m k) \ y < poly_mapping_size m" using keys_less_poly_mapping_size by (auto intro: le_less_trans)
lemma poly_mapping_size_estimation2: assumes"v \ range m" and "y \ g v" shows"y < poly_mapping_size m" proof - from assms obtain k where *: "lookup m k = v""v \ 0" by transfer blast thenhave"k \ keys m" by (simp add: in_keys_iff) with * show ?thesis by (simp add: Poly_Mapping.poly_mapping_size_estimation assms(2) trans_le_add2) qed
end
lemma poly_mapping_size_one [simp]: "poly_mapping_size f g 1 = g 0 + f 0 + g 1 + 1" unfolding poly_mapping_size_def by transfer simp
lemma poly_mapping_size_cong [fundef_cong]: "m = m' \ g 0 = g' 0 \ (\k. k \ keys m' \ f k = f' k) \<Longrightarrow> (\<And>v. v \<in> range m' \<Longrightarrow> g v = g' v) \<Longrightarrow> poly_mapping_size f g m = poly_mapping_size f' g' m'" by (auto simp: poly_mapping_size_def intro!: sum.cong)
instantiation poly_mapping :: (type, zero) size begin
subsection \<open>Further mapping operations and properties\<close>
text\<open>It is like in algebra: there are many definitions, some are also used\<close>
lift_definition mapp :: "('a \ 'b :: zero \ 'c :: zero) \ ('a \\<^sub>0 'b) \ ('a \\<^sub>0 'c)" is"\f p k. (if k \ keys p then f k (lookup p k) else 0)" by simp
lemma mapp_cong [fundef_cong]: "\ m = m'; \k. k \ keys m' \ f k (lookup m' k) = f' k (lookup m' k) \ \<Longrightarrow> mapp f m = mapp f' m'" by transfer (auto simp: fun_eq_iff)
lemma lookup_mapp: "lookup (mapp f p) k = (f k (lookup p k) when k \ keys p)" by (simp add: mapp.rep_eq)
lemma keys_mapp_subset: "keys (mapp f p) \ keys p" by (meson in_keys_iff mapp.rep_eq subsetI)
subsection\<open>Free Abelian Groups Over a Type\<close>
abbreviation frag_of :: "'a \ 'a \\<^sub>0 int" where"frag_of c \ Poly_Mapping.single c (1::int)"
lemma lookup_frag_of [simp]: "Poly_Mapping.lookup(frag_of c) = (\x. if x = c then 1 else 0)" by (force simp add: lookup_single_not_eq)
lemma frag_of_nonzero [simp]: "frag_of a \ 0" by (metis lookup_single_eq lookup_zero zero_neq_one)
definition frag_cmul :: "int \ ('a \\<^sub>0 int) \ ('a \\<^sub>0 int)" where"frag_cmul c a = Abs_poly_mapping (\x. c * Poly_Mapping.lookup a x)"
lemma frag_cmul_zero [simp]: "frag_cmul 0 x = 0" by (simp add: frag_cmul_def)
lemma frag_cmul_zero2 [simp]: "frag_cmul c 0 = 0" by (simp add: frag_cmul_def)
lemma frag_cmul_one [simp]: "frag_cmul 1 x = x" by (simp add: frag_cmul_def)
lemma frag_cmul_minus_one [simp]: "frag_cmul (-1) x = -x" by (simp add: frag_cmul_def uminus_poly_mapping_def poly_mapping_eqI)
lemma frag_cmul_cmul [simp]: "frag_cmul c (frag_cmul d x) = frag_cmul (c*d) x" by (simp add: frag_cmul_def mult_ac)
lemma lookup_frag_cmul [simp]: "poly_mapping.lookup (frag_cmul c x) i = c * poly_mapping.lookup x i" by (simp add: frag_cmul_def)
lemma minus_frag_cmul [simp]: "- frag_cmul k x = frag_cmul (-k) x" by (simp add: poly_mapping_eqI)
lemma keys_frag_of: "Poly_Mapping.keys(frag_of a) = {a}" by simp
lemma finite_cmul_nonzero: "finite {x. c * Poly_Mapping.lookup a x \ (0::int)}" by simp
lemma keys_cmul: "Poly_Mapping.keys(frag_cmul c a) \ Poly_Mapping.keys a" using finite_cmul_nonzero [of c a] by (metis lookup_frag_cmul mult_zero_right not_in_keys_iff_lookup_eq_zero subsetI)
lemma keys_cmul_iff [iff]: "i \ Poly_Mapping.keys (frag_cmul c x) \ i \ Poly_Mapping.keys x \ c \ 0" by (metis in_keys_iff lookup_frag_cmul mult_eq_0_iff)
lemma keys_diff: "Poly_Mapping.keys(a - b) \ Poly_Mapping.keys a \ Poly_Mapping.keys b" by (auto simp: in_keys_iff lookup_minus)
lemma keys_eq_empty [simp]: "Poly_Mapping.keys c = {} \ c = 0" by (metis in_keys_iff keys_zero lookup_zero poly_mapping_eqI)
lemma frag_cmul_eq_0_iff [simp]: "frag_cmul k c = 0 \ k=0 \ c=0" by auto (metis subsetI subset_antisym keys_cmul_iff keys_eq_empty)
lemma frag_of_eq: "frag_of x = frag_of y \ x = y" by (metis lookup_single_eq lookup_single_not_eq zero_neq_one)
lemma frag_cmul_distrib: "frag_cmul (c+d) a = frag_cmul c a + frag_cmul d a" by (simp add: frag_cmul_def plus_poly_mapping_def int_distrib)
lemma frag_cmul_distrib2: "frag_cmul c (a+b) = frag_cmul c a + frag_cmul c b" by (simp add: int_distrib(2) lookup_add poly_mapping_eqI)
lemma frag_cmul_diff_distrib: "frag_cmul (a - b) c = frag_cmul a c - frag_cmul b c" by (auto simp: left_diff_distrib lookup_minus poly_mapping_eqI)
lemma frag_cmul_sum: "frag_cmul a (sum b I) = (\i\I. frag_cmul a (b i))" proof (induction rule: infinite_finite_induct) case (insert i I) thenshow ?case by (auto simp: algebra_simps frag_cmul_distrib2) qed auto
lemma keys_sum: "Poly_Mapping.keys(sum b I) \ (\i \I. Poly_Mapping.keys(b i))" proof (induction I rule: infinite_finite_induct) case (insert i I) thenshow ?case using keys_add [of "b i""sum b I"] by auto qed auto
definition frag_extend :: "('b \ 'a \\<^sub>0 int) \ ('b \\<^sub>0 int) \ 'a \\<^sub>0 int" where"frag_extend b x \ (\i \ Poly_Mapping.keys x. frag_cmul (Poly_Mapping.lookup x i) (b i))"
lemma frag_extend_0 [simp]: "frag_extend b 0 = 0" by (simp add: frag_extend_def)
lemma frag_extend_of [simp]: "frag_extend f (frag_of a) = f a" by (simp add: frag_extend_def)
lemma frag_extend_cmul: "frag_extend f (frag_cmul c x) = frag_cmul c (frag_extend f x)" by (auto simp: frag_extend_def frag_cmul_sum intro: sum.mono_neutral_cong_left)
lemma frag_extend_minus: "frag_extend f (- x) = - (frag_extend f x)" using frag_extend_cmul [of f "-1"] by simp
lemma frag_extend_add: "frag_extend f (a+b) = (frag_extend f a) + (frag_extend f b)" proof - have *: "(\i\Poly_Mapping.keys a. frag_cmul (poly_mapping.lookup a i) (f i))
= (\<Sum>i\<in>Poly_Mapping.keys a \<union> Poly_Mapping.keys b. frag_cmul (poly_mapping.lookup a i) (f i))" "(\i\Poly_Mapping.keys b. frag_cmul (poly_mapping.lookup b i) (f i))
= (\<Sum>i\<in>Poly_Mapping.keys a \<union> Poly_Mapping.keys b. frag_cmul (poly_mapping.lookup b i) (f i))" by (auto simp: in_keys_iff intro: sum.mono_neutral_cong_left) have"frag_extend f (a+b) = (\i\Poly_Mapping.keys (a + b).
frag_cmul (poly_mapping.lookup a i) (f i) + frag_cmul (poly_mapping.lookup b i) (f i)) " by (auto simp: frag_extend_def Poly_Mapping.lookup_add frag_cmul_distrib) alsohave"... = (\i \ Poly_Mapping.keys a \ Poly_Mapping.keys b. frag_cmul (poly_mapping.lookup a i) (f i)
+ frag_cmul (poly_mapping.lookup b i) (f i))" proof (rule sum.mono_neutral_cong_left) show"\i\keys a \ keys b - keys (a + b).
frag_cmul (lookup a i) (f i) + frag_cmul (lookup b i) (f i) = 0" by (metis DiffD2 frag_cmul_distrib frag_cmul_zero in_keys_iff lookup_add) qed (auto simp: keys_add) alsohave"... = (frag_extend f a) + (frag_extend f b)" by (auto simp: * sum.distrib frag_extend_def) finallyshow ?thesis . qed
lemma frag_extend_diff: "frag_extend f (a-b) = (frag_extend f a) - (frag_extend f b)" by (metis (no_types, opaque_lifting) add_uminus_conv_diff frag_extend_add frag_extend_minus)
lemma frag_extend_sum: "finite I \ frag_extend f (\i\I. g i) = sum (frag_extend f o g) I" by (induction I rule: finite_induct) (simp_all add: frag_extend_add)
lemma frag_extend_eq: "(\f. f \ Poly_Mapping.keys c \ g f = h f) \ frag_extend g c = frag_extend h c" by (simp add: frag_extend_def)
lemma frag_extend_eq_0: "(\x. x \ Poly_Mapping.keys c \ f x = 0) \ frag_extend f c = 0" by (simp add: frag_extend_def)
lemma keys_frag_extend: "Poly_Mapping.keys(frag_extend f c) \ (\x \ Poly_Mapping.keys c. Poly_Mapping.keys(f x))" unfolding frag_extend_def using keys_sum by fastforce
lemma frag_expansion: "a = frag_extend frag_of a" proof - have *: "finite I \<Longrightarrow> Poly_Mapping.lookup (\<Sum>i\<in>I. frag_cmul (Poly_Mapping.lookup a i) (frag_of i)) j =
(if j \<in> I then Poly_Mapping.lookup a j else 0)" for I j by (induction I rule: finite_induct) (auto simp: lookup_single lookup_add) show ?thesis unfolding frag_extend_def by (rule poly_mapping_eqI) (fastforce simp add: in_keys_iff *) qed
lemma frag_closure_minus_cmul: assumes"P 0"and P: "\x y. \P x; P y\ \ P(x - y)" "P c" shows"P(frag_cmul k c)" proof - have"P (frag_cmul (int n) c)"for n proof (induction n) case 0 thenshow ?case by (simp add: assms) next case (Suc n) thenshow ?case by (metis assms diff_0 diff_minus_eq_add frag_cmul_distrib frag_cmul_one of_nat_Suc) qed thenshow ?thesis by (metis (no_types, opaque_lifting) add_diff_eq assms(2) diff_add_cancel frag_cmul_distrib int_diff_cases) qed
lemma frag_induction [consumes 1, case_names zero one diff]: assumes supp: "Poly_Mapping.keys c \ S" and 0: "P 0"and sing: "\x. x \ S \ P(frag_of x)" and diff: "\a b. \P a; P b\ \ P(a - b)" shows"P c" proof -
--> --------------------
--> maximum size reached
--> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.35Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
