# Theory Deriv_PDeriv

```(*  Author: Tobias Nipkow, Dmitriy Traytel *)

section "Connection Between Derivatives and Partial Derivatives"

(*<*)
theory Deriv_PDeriv
imports Derivatives_Finite
begin
(*>*)

lemma pderiv_not_is_Zero_is_Plus[simp]: "∀x ∈ pderiv a r. ¬ is_Zero x ∧ ¬ is_Plus x"
by (induct r) auto

lemma finite_pderiv[simp]: "finite (pderiv a r)"
by (induct r) auto

lemma PLUS_inject: "⟦∀x ∈ set xs ∪ set ys. ¬ is_Zero x ∧ ¬ is_Plus x; sorted xs; sorted ys⟧ ⟹
(PLUS xs = PLUS ys) ⟷ xs = ys"
proof (induct xs arbitrary: ys rule: list_singleton_induct)
case nil then show ?case by (induct ys rule: list_singleton_induct) auto
next
case single then show ?case by (induct ys rule: list_singleton_induct) auto
next
case cons then show ?case by (induct ys rule: list_singleton_induct) auto
qed

lemma sorted_list_of_set_inject: "⟦finite R; finite S⟧ ⟹
(sorted_list_of_set R = sorted_list_of_set S) ⟷ R = S"
proof (induct R arbitrary: S rule: finite_linorder_min_induct)
case empty then show ?case
proof (induct S rule: finite_linorder_min_induct)
case (insert b S) then show ?case by simp (metis insort_not_Nil)
qed simp
next
case (insert a R) from this(4,1-3) show ?case
proof (induct S rule: finite_linorder_min_induct)
case (insert b S)
show ?case
proof
assume "sorted_list_of_set (insert a R) = sorted_list_of_set (insert b S)"
with insert(1,2,4,5) have "insort a (sorted_list_of_set R) = insort b (sorted_list_of_set S)"
by fastforce
with insert(2,5) have "a # sorted_list_of_set R = b # sorted_list_of_set S"
apply (cases "sorted_list_of_set R" "sorted_list_of_set S" rule: list.exhaust[case_product list.exhaust])
apply (auto split: if_splits simp add: not_le)
using insort_not_Nil apply metis
using insert.prems(1) set_sorted_list_of_set apply fastforce
using insert.prems(1) set_sorted_list_of_set apply fastforce
using insert.prems(1) set_sorted_list_of_set apply fastforce
using insert.hyps(1) set_sorted_list_of_set apply fastforce
using insert.hyps(1) set_sorted_list_of_set apply fastforce
using insert.hyps(1) set_sorted_list_of_set apply fastforce
using insert.hyps(1) set_sorted_list_of_set apply fastforce
using insert.hyps(1) set_sorted_list_of_set apply fastforce
done
with insert show "insert a R = insert b S" by auto
next
assume "insert a R = insert b S"
then show "sorted_list_of_set (insert a R) = sorted_list_of_set (insert b S)" by simp
qed
qed simp
qed

lemma flatten_PLUS_inject: "⟦∀x ∈ R ∪ S. ¬ is_Zero x ∧ ¬ is_Plus x; finite R; finite S⟧ ⟹
(flatten PLUS R = flatten PLUS S) = (R = S)"
by (rule trans[OF PLUS_inject sorted_list_of_set_inject]) auto

primrec pset where
"pset Zero = {}"
| "pset One = {One}"
| "pset (Atom a) = {Atom a}"
| "pset (Plus r s) = pset r ∪ pset s"
| "pset (Times r s) = Timess (pset r) s"
| "pset (Star r) = {Star r}"

lemma pset_not_is_Zero_is_Plus[simp]: "∀x ∈ pset r. ¬ is_Zero x ∧ ¬ is_Plus x"
by (induct r) auto

lemma finite_pset[simp]: "finite (pset r)"
by (induct r) auto

lemma pset_deriv: "pset (deriv a r) = pderiv a r"
by (induct r) auto

definition pnorm where
"pnorm = flatten PLUS o pset"

lemma pnorm_deriv_eq_iff_pderiv_eq:
"pnorm (deriv a r) = pnorm (deriv a s) ⟷ pderiv a r = pderiv a s"
unfolding pnorm_def o_apply pset_deriv
by (rule flatten_PLUS_inject) auto

fun pnPlus :: "'a::linorder rexp ⇒ 'a rexp ⇒ 'a rexp" where
"pnPlus Zero r = r"
| "pnPlus r Zero = r"
| "pnPlus (Plus r s) t = pnPlus r (pnPlus s t)"
| "pnPlus r (Plus s t) =
(if r = s then (Plus s t)
else if le_rexp r s then Plus r (Plus s t)
else Plus s (pnPlus r t))"
| "pnPlus r s =
(if r = s then r
else if le_rexp r s then Plus r s
else Plus s r)"

fun pnTimes :: "'a::linorder rexp ⇒ 'a rexp ⇒ 'a rexp" where
"pnTimes Zero r = Zero"
| "pnTimes (Plus r s) t = pnPlus (pnTimes r t) (pnTimes s t)"
| "pnTimes r s = Times r s"

primrec pnorm_alt :: "'a::linorder rexp ⇒ 'a rexp" where
"pnorm_alt Zero = Zero"
| "pnorm_alt One = One"
| "pnorm_alt (Atom a) = Atom a"
| "pnorm_alt (Plus r s) = pnPlus (pnorm_alt r) (pnorm_alt s)"
| "pnorm_alt (Times r s) = pnTimes (pnorm_alt r) s"
| "pnorm_alt (Star r) = Star r"

lemma pset_pnPlus:
"pset (pnPlus r s) = pset (Plus r s)"
by (induct r s rule: pnPlus.induct) auto

lemma pset_pnTimes:
"pset (pnTimes r s) = pset (Times r s)"
by (induct r s rule: pnTimes.induct) (auto simp: pset_pnPlus)

lemma pset_pnorm_alt_Times: "s ∈ pset r ⟹ pnTimes (pnorm_alt s) t = Times (pnorm_alt s) t"
by (induct r arbitrary: s t) auto

lemma pset_pnorm_alt:
"pset (pnorm_alt r) = pnorm_alt ` pset r"
by (induct r) (auto simp: pset_pnPlus pset_pnTimes pset_pnorm_alt_Times image_iff)

lemma pset_pnTimes_Times: "s ∈ pset r ⟹ pnTimes s t = Times s t"
by (induct r arbitrary: s t) auto

lemma pset_pnorm_alt_id: "s ∈ pset r ⟹ pnorm_alt s = s"
by (induct r arbitrary: s) (auto simp: pset_pnTimes_Times)

lemma pnorm_alt_image_pset: "pnorm_alt ` pset r = pset r"
by (induction r) (auto, auto simp add: pset_pnorm_alt_id pset_pnTimes_Times image_iff)

lemma pnorm_pnorm_alt: "pnorm (pnorm_alt r) = pnorm r"
by (induct r) (auto simp: pnorm_def pset_pnPlus pset_pnTimes pset_pnorm_alt pnorm_alt_image_pset)

lemma pnPlus_singleton_PLUS:
"⟦xs ≠ []; sorted xs; distinct xs; ∀x ∈ {x} ∪ set xs. ¬is_Zero x ∧ ¬is_Plus x⟧ ⟹
pnPlus x (PLUS xs) = (if x ∈ set xs then PLUS xs else PLUS (insort x xs))"
proof (induct xs rule: list_singleton_induct)
case (single y)
thus ?case unfolding is_Zero_def is_Plus_def
apply (cases x y rule: linorder_cases)
apply (induct x y rule: pnPlus.induct)
apply (auto simp: less_rexp_def less_eq_rexp_def)
apply (cases y)
apply auto
apply (induct x y rule: pnPlus.induct)
apply (auto simp: less_rexp_def less_eq_rexp_def)
apply (induct x y rule: pnPlus.induct)
apply (auto simp: less_rexp_def less_eq_rexp_def)
done
next
case (cons y1 y2 ys) thus ?case unfolding is_Zero_def is_Plus_def
apply (cases x)
apply (metis UnCI insertI1)
apply simp apply (metis antisym less_eq_rexp_def)
apply simp apply (metis antisym less_eq_rexp_def)
apply (metis UnCI insertI1)
apply simp apply (metis antisym less_eq_rexp_def)
apply simp apply (metis antisym less_eq_rexp_def)
done
qed simp

lemma pnPlus_PlusL[simp]: "t ≠ Zero ⟹ pnPlus (Plus r s) t = pnPlus r (pnPlus s t)"
by (induct t) auto

lemma pnPlus_ZeroR[simp]: "pnPlus r Zero = r"
by (induct r) auto

lemma PLUS_eq_Zero: "PLUS xs = Zero ⟷ xs = [] ∨ xs = [Zero]"
by (induct xs rule: list_singleton_induct) auto

lemma pnPlus_PLUS:
"⟦xs1 ≠ []; xs2 ≠ []; ∀x ∈ set (xs1 @ xs2). ¬is_Zero x ∧ ¬is_Plus x; sorted xs2; distinct xs2⟧⟹
pnPlus (PLUS xs1) (PLUS xs2) = flatten PLUS (set (xs1 @ xs2))"
proof (induct xs1 arbitrary: xs2 rule: list_singleton_induct)
case (single x1)
thus ?case
apply (auto intro!: trans[OF pnPlus_singleton_PLUS]
simp: insert_absorb simp del: sorted_list_of_set_insert_remove)
apply (metis List.finite_set finite_sorted_distinct_unique sorted_list_of_set)
apply (rule arg_cong[of _ _ PLUS])
apply (metis remdups_id_iff_distinct sorted_list_of_set_sort_remdups sorted_sort_id)
done
next
case (cons x11 x12 xs1)
then show ?case unfolding rexp_of_list.simps
apply (subst pnPlus_PlusL)
apply (unfold PLUS_eq_Zero) []
apply (metis in_set_conv_decomp rexp.disc(1))
apply (subst cons(1))
apply (simp_all del: sorted_list_of_set_insert_remove)
apply (rule trans[OF pnPlus_singleton_PLUS])
apply (simp_all add: sorted_insort set_insort_key del: sorted_list_of_set_insert_remove)
apply safe
unfolding insert_commute[of x11]
apply (auto simp only: Un_insert_left[of x11, symmetric] insert_absorb) []
apply (auto simp only: Un_insert_right[of _ x11, symmetric] insert_absorb) []
done
qed simp

lemma pnPlus_flatten_PLUS:
"⟦X1 ≠ {}; X2 ≠ {}; finite X1; finite X2; ∀x ∈ X1 ∪ X2.  ¬is_Zero x ∧ ¬is_Plus x⟧⟹
pnPlus (flatten PLUS X1) (flatten PLUS X2) = flatten PLUS (X1 ∪ X2)"
by (rule trans[OF pnPlus_PLUS]) auto

lemma pnPlus_pnorm: "pnPlus (pnorm r) (pnorm s) = pnorm (Plus r s)"
by (cases "pset r = {} ∨ pset s = {}")
(auto simp: pnorm_def pset_pnPlus pset_pnorm_alt intro: pnPlus_flatten_PLUS)

lemma pnTimes_not_Zero_or_Plus[simp]: "⟦¬ is_Zero x; ¬ is_Plus x⟧ ⟹ pnTimes x r = Times x r"
by (cases x) auto

lemma pnTimes_PLUS:
"⟦xs ≠ []; ∀x ∈ set xs. ¬is_Zero x ∧ ¬is_Plus x⟧⟹
pnTimes (PLUS xs) r = flatten PLUS (Timess (set xs) r)"
proof (induct xs arbitrary: r rule: list_singleton_induct)
case (cons x y xs) then show ?case unfolding rexp_of_list.simps pnTimes.simps
apply (subst pnTimes_not_Zero_or_Plus)
apply (simp_all add: sorted_insort set_insort_key del: sorted_list_of_set_insert_remove)
apply (subst pnPlus_singleton_PLUS)
apply (simp_all add: sorted_insort set_insort_key del: sorted_list_of_set_insert_remove)
unfolding insert_commute[of "Times y r"]
apply (simp del: sorted_list_of_set_insert_remove)
apply safe
apply (subst insert_absorb[of "Times x r"])
apply simp_all
done
qed auto

lemma pnTimes_flatten_PLUS:
"⟦X1 ≠ {}; finite X1; ∀x ∈ X1. ¬is_Zero x ∧ ¬is_Plus x⟧⟹
pnTimes (flatten PLUS X1) r = flatten PLUS (Timess X1 r)"
by (rule trans[OF pnTimes_PLUS]) auto

lemma pnTimes_pnorm: "pnTimes (pnorm r1) r2 = pnorm (Times r1 r2)"
by (cases "pset r1 = {}")
(auto simp: pnorm_def pset_pnTimes pset_pnorm_alt intro: pnTimes_flatten_PLUS)

lemma pnorm_alt[symmetric]: "pnorm_alt r = pnorm r"
by (induct r) (simp_all only: pnorm_alt.simps pnPlus_pnorm pnTimes_pnorm, auto simp: pnorm_def)

lemma insort_eq_Cons: "⟦∀a ∈ set xs. b < a; sorted xs⟧ ⟹ insort b xs = b # xs"
by (cases xs) auto

lemma pderiv_PLUS: "pderiv a (PLUS (x # xs)) = pderiv a x ∪ pderiv a (PLUS xs)"
by (cases xs) auto

lemma pderiv_set_flatten_PLUS:
"finite X ⟹ pderiv (a :: 'a :: linorder) (flatten PLUS X) = pderiv_set a X"
proof (induction X rule: finite_linorder_min_induct)
case (insert b X)
then have "b ∉ X" by auto
then have "pderiv a (flatten PLUS (insert b X)) = pderiv a b ∪ pderiv a (flatten PLUS X)"
by (simp add: pderiv_PLUS insort_eq_Cons insert.hyps)
also from insert.IH have "… = pderiv a b ∪ pderiv_set a X" by simp
finally show ?case by simp
qed simp

lemma fold_pderiv_set_flatten_PLUS:
"⟦w ≠ []; finite X⟧ ⟹ fold pderiv_set w {flatten PLUS X} = fold pderiv_set w X"
by (induct w arbitrary: X) (simp_all add: pderiv_set_flatten_PLUS)

lemma fold_pnorm_deriv:
"fold (λa r. pnorm (deriv a r)) w s = flatten PLUS (fold pderiv_set w {s})"
proof (induction w arbitrary: s)
case (Cons x w) then show ?case
proof (cases "w = []")
case False
show ?thesis using fold_pderiv_set_flatten_PLUS[OF False] Cons.IH
by (auto simp: pnorm_def pset_deriv)
qed simp

primrec
pnderiv :: "'a :: linorder ⇒ 'a rexp ⇒ 'a rexp"
where
"pnderiv c (Zero) = Zero"
| "pnderiv c (One) = Zero"
| "pnderiv c (Atom c') = (if c = c' then One else Zero)"
| "pnderiv c (Plus r1 r2) = pnPlus (pnderiv c r1) (pnderiv c r2)"
| "pnderiv c (Times r1 r2) =
(if nullable r1 then pnPlus (pnTimes (pnderiv c r1) r2) (pnderiv c r2) else pnTimes (pnderiv c r1) r2)"
| "pnderiv c (Star r) = pnTimes (pnderiv c r) (Star r)"

lemma pnderiv_alt[code]: "pnderiv a r = pnorm (deriv a r)"
by (induct r) (auto simp: pnorm_alt)

lemma pnderiv_pderiv: "pnderiv a r = flatten PLUS (pderiv a r)"
unfolding pnderiv_alt pnorm_def o_apply pset_deriv ..

(*<*)
end
(*>*)
```