[STATEMENT]
lemma prod_fun_max:
  fixes f g :: "'a::{linorder, ordered_cancel_comm_monoid_add} \<Rightarrow> 'b::semiring_0"
  assumes zero: "\<And>m. m > a \<Longrightarrow> f m = 0" "\<And>m. m > b \<Longrightarrow> g m = 0"
  assumes fin: "finite {m. f m \<noteq> 0}" "finite {m. g m \<noteq> 0}"
  shows   "prod_fun f g (a + b) = f a * g b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
note fin' = finite_subset[OF _ fin(1)] finite_subset[OF _ fin(2)]
[PROOF STATE]
proof (state)
this:
?A \<subseteq> {m. f m \<noteq> (0::'b)} \<Longrightarrow> finite ?A
?A \<subseteq> {m. g m \<noteq> (0::'b)} \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
have "prod_fun f g (a + b) = (\<Sum>l. f l * (\<Sum>q. g q when a + b = l + q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod_fun f g (a + b) = (\<Sum>l. f l * (\<Sum>q. g q when a + b = l + q))
[PROOF STEP]
by (simp add: prod_fun_def Sum_any_right_distrib)
[PROOF STATE]
proof (state)
this:
prod_fun f g (a + b) = (\<Sum>l. f l * (\<Sum>q. g q when a + b = l + q))

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
prod_fun f g (a + b) = (\<Sum>l. f l * (\<Sum>q. g q when a + b = l + q))

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
have "\<dots> = (\<Sum>l. \<Sum>q. f l * g q when a + b = l + q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>l. f l * (\<Sum>q. g q when a + b = l + q)) = (\<Sum>l. \<Sum>q. f l * g q when a + b = l + q)
[PROOF STEP]
by (subst Sum_any_right_distrib) (auto intro!: Sum_any.cong fin'(2) simp: when_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>l. f l * (\<Sum>q. g q when a + b = l + q)) = (\<Sum>l. \<Sum>q. f l * g q when a + b = l + q)

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>l. f l * (\<Sum>q. g q when a + b = l + q)) = (\<Sum>l. \<Sum>q. f l * g q when a + b = l + q)

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(\<Sum>l. f l * (\<Sum>q. g q when a + b = l + q)) = (\<Sum>l. \<Sum>q. f l * g q when a + b = l + q)

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
fix l q
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
assume lq: "a + b = l + q" "(a, b) \<noteq> (l, q)" and nz: "f l * g q \<noteq> 0"
[PROOF STATE]
proof (state)
this:
a + b = l + q
(a, b) \<noteq> (l, q)
f l * g q \<noteq> (0::'b)

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
from nz and zero
[PROOF STATE]
proof (chain)
picking this:
f l * g q \<noteq> (0::'b)
a < ?m \<Longrightarrow> f ?m = (0::'b)
b < ?m \<Longrightarrow> g ?m = (0::'b)
[PROOF STEP]
have "l \<le> a" "q \<le> b"
[PROOF STATE]
proof (prove)
using this:
f l * g q \<noteq> (0::'b)
a < ?m \<Longrightarrow> f ?m = (0::'b)
b < ?m \<Longrightarrow> g ?m = (0::'b)

goal (1 subgoal):
 1. l \<le> a &&& q \<le> b
[PROOF STEP]
by (auto intro: leI)
[PROOF STATE]
proof (state)
this:
l \<le> a
q \<le> b

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
l \<le> a
q \<le> b

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
from this and lq(2)
[PROOF STATE]
proof (chain)
picking this:
l \<le> a
q \<le> b
(a, b) \<noteq> (l, q)
[PROOF STEP]
have "l < a \<or> q < b"
[PROOF STATE]
proof (prove)
using this:
l \<le> a
q \<le> b
(a, b) \<noteq> (l, q)

goal (1 subgoal):
 1. l < a \<or> q < b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l < a \<or> q < b

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
l \<le> a
q \<le> b
l < a \<or> q < b
[PROOF STEP]
have "l + q < a + b"
[PROOF STATE]
proof (prove)
using this:
l \<le> a
q \<le> b
l < a \<or> q < b

goal (1 subgoal):
 1. l + q < a + b
[PROOF STEP]
by (auto intro: add_less_le_mono add_le_less_mono)
[PROOF STATE]
proof (state)
this:
l + q < a + b

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
with lq(1)
[PROOF STATE]
proof (chain)
picking this:
a + b = l + q
l + q < a + b
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
a + b = l + q
l + q < a + b

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>a + b = ?l2 + ?q2; (a, b) \<noteq> (?l2, ?q2); f ?l2 * g ?q2 \<noteq> (0::'b)\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
hence "(\<Sum>l. \<Sum>q. f l * g q when a + b = l + q) = (\<Sum>l. \<Sum>q. f l * g q when (a, b) = (l, q))"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a + b = ?l2 + ?q2; (a, b) \<noteq> (?l2, ?q2); f ?l2 * g ?q2 \<noteq> (0::'b)\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. (\<Sum>l. \<Sum>q. f l * g q when a + b = l + q) = (\<Sum>l. \<Sum>q. f l * g q when (a, b) = (l, q))
[PROOF STEP]
by (intro Sum_any.cong refl) (auto simp: when_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>l. \<Sum>q. f l * g q when a + b = l + q) = (\<Sum>l. \<Sum>q. f l * g q when (a, b) = (l, q))

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>l. \<Sum>q. f l * g q when a + b = l + q) = (\<Sum>l. \<Sum>q. f l * g q when (a, b) = (l, q))

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
have "\<dots> = (\<Sum>(l,q). f l * g q when (a, b) = (l, q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>l. \<Sum>q. f l * g q when (a, b) = (l, q)) = (\<Sum>(l, q). f l * g q when (a, b) = (l, q))
[PROOF STEP]
by (intro Sum_any.cartesian_product[of "{(a, b)}"]) auto
[PROOF STATE]
proof (state)
this:
(\<Sum>l. \<Sum>q. f l * g q when (a, b) = (l, q)) = (\<Sum>(l, q). f l * g q when (a, b) = (l, q))

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>l. \<Sum>q. f l * g q when (a, b) = (l, q)) = (\<Sum>(l, q). f l * g q when (a, b) = (l, q))

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
have "\<dots> = (\<Sum>(l,q)\<in>{(a,b)}. f l * g q when (a, b) = (l, q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(l, q). f l * g q when (a, b) = (l, q)) = (\<Sum>(l, q)\<in>{(a, b)}. f l * g q when (a, b) = (l, q))
[PROOF STEP]
by (intro Sum_any.expand_superset) auto
[PROOF STATE]
proof (state)
this:
(\<Sum>(l, q). f l * g q when (a, b) = (l, q)) = (\<Sum>(l, q)\<in>{(a, b)}. f l * g q when (a, b) = (l, q))

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>(l, q). f l * g q when (a, b) = (l, q)) = (\<Sum>(l, q)\<in>{(a, b)}. f l * g q when (a, b) = (l, q))

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
have "\<dots> = f a * g b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(l, q)\<in>{(a, b)}. f l * g q when (a, b) = (l, q)) = f a * g b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>(l, q)\<in>{(a, b)}. f l * g q when (a, b) = (l, q)) = f a * g b

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
prod_fun f g (a + b) = f a * g b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
prod_fun f g (a + b) = f a * g b

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
prod_fun f g (a + b) = f a * g b

goal:
No subgoals!
[PROOF STEP]
qed