Theory CRT_Product_Tree
section ‹Product and remainder trees›
theory CRT_Product_Tree
imports "HOL-Number_Theory.Number_Theory"
begin
subsection ‹Auxiliary material›
lemma mset_diff_irrelevant [simp]: "x ∉# Y ⟹ x ∈# X - Y ⟷ x ∈# X"
by (simp add: in_diff_count not_in_iff)
context semiring_gcd
begin
lemma prod_mset_coprime_left:
"coprime (prod_mset X) a" if "⋀x. x ∈# X ⟹ coprime x a"
using that by (induct X) auto
lemma prod_mset_coprime_right:
"coprime a (prod_mset X)" if "⋀x. x ∈# X ⟹ coprime a x"
using coprime_commute prod_mset_coprime_left that by presburger
end
lemma modular_inverse_cong:
fixes x x' m :: "'a :: {unique_euclidean_ring, euclidean_ring_gcd}"
assumes "[x = x'] (mod m)" "coprime m x"
shows "modular_inverse m x = modular_inverse m x'"
proof -
have x': "coprime m x'"
using assms(1,2) cong_imp_coprime coprime_commute by blast
have "[modular_inverse m x * x = 1] (mod m)"
by (rule cong_modular_inverse2) (use assms in ‹auto simp: coprime_commute›)
also have "[1 = modular_inverse m x' * x'] (mod m)"
by (rule cong_sym, rule cong_modular_inverse2) (use x' in ‹auto simp: coprime_commute›)
also have "[modular_inverse m x' * x' = modular_inverse m x' * x] (mod m)"
by (intro cong_mult cong_refl cong_sym[OF assms(1)])
finally have "[modular_inverse m x = modular_inverse m x'] (mod m)"
using ‹coprime m x› by (simp add: cong_mult_rcancel coprime_commute)
thus ?thesis
by (auto simp: cong_def modular_inverse_def)
qed
lemma cong_sum_list:
assumes "list_all2 (λx y. [x = y] (mod m)) xs ys"
shows "[sum_list xs = sum_list ys] (mod m)"
using assms by induction (auto intro!: cong_add)
lemma cong_sum_list':
assumes "list_all2 (λx y. [f x = g y] (mod m)) xs ys"
shows "[sum_list (map f xs) = sum_list (map g ys)] (mod m)"
using assms by induction (auto intro!: cong_add)
lemma sorted_wrt_symD:
assumes "sorted_wrt P xs" "P x y ⟷ P y x"
assumes "x ∈ set xs" "y ∈ set xs" "x ≠ y"
shows "P x y"
using assms by (induction xs) auto
subsection ‹Prerequisite: A ``pairwise'' operator for multisets›
text ‹
The following is a multiset analogue of the \<^const>‹pairwise› operator for sets.
›
definition pairwise_mset :: "('a ⇒ 'a ⇒ bool) ⇒ 'a multiset ⇒ bool" where
"pairwise_mset P X ⟷ (∀x∈#X. ∀y∈#X-{#x#}. P x y)"
lemma pairwise_msetI: "(⋀x y. x ∈# X ⟹ y ∈# X - {#x#} ⟹ P x y) ⟹ pairwise_mset P X"
by (auto simp: pairwise_mset_def)
lemma pairwise_msetI': "(⋀x y. {#x, y#} ⊆# X ⟹ P x y) ⟹ pairwise_mset P X"
by (rule pairwise_msetI) (auto simp: insert_subset_eq_iff)
lemma pairwise_msetD: "pairwise_mset P X ⟹ x ∈# X ⟹ y ∈# X - {#x#} ⟹ P x y"
by (auto simp: pairwise_mset_def)
lemma pairwise_msetD': "pairwise_mset P X ⟹ {#x, y#} ⊆# X ⟹ P x y"
by (erule pairwise_msetD) (auto simp: insert_subset_eq_iff)
lemma pairwise_mset_empty [simp, intro]: "pairwise_mset P {#}"
by (auto simp: pairwise_mset_def)
lemma pairwise_mset_singleton [simp, intro]: "pairwise_mset P {#x#}"
by (auto simp: pairwise_mset_def)
lemma pairwise_mset_doubleton_iff [simp]: "pairwise_mset P {#x, y#} ⟷ P x y ∧ P y x"
by (auto simp: pairwise_mset_def)
lemma pairwise_mset_add_mset:
"pairwise_mset P (add_mset x X) ⟷ pairwise_mset P X ∧ (∀y∈#X. P x y ∧ P y x)"
by (auto simp: pairwise_mset_def)
lemma pairwise_mset_plus:
"pairwise_mset P (X + Y) ⟷ pairwise_mset P X ∧ pairwise_mset P Y ∧ (∀x∈#X. ∀y∈#Y. P x y ∧ P y x)"
by (induction Y) (auto simp: pairwise_mset_add_mset)
lemma pairwise_mset_mono:
"pairwise_mset P X ⟹ (⋀x y. x ∈# Y ⟹ y ∈# Y - {#x#} ⟹ P x y ⟹ Q x y) ⟹ Y ⊆# X ⟹ pairwise_mset Q Y"
unfolding pairwise_mset_def by (metis insert_DiffM insert_subset_eq_iff)
lemma sorted_wrt_sym_conv_pairwise_mset:
assumes "⋀x y. x ∈ set xs ⟹ y ∈ set xs ⟹ P x y ⟷ P y x"
shows "sorted_wrt P xs ⟷ pairwise_mset P (mset xs)"
using assms by (induction xs) (auto simp: pairwise_mset_add_mset)
subsection ‹Definition of product trees›
text ‹
A product tree in the classical sense is a binary tree that has a non-zero number attached to
each leaf and each internal node has the product of its two immediate child nodes attached to it.
We use a slightly more general structure which can carry additional information at the leaves
as well. We also introduce a relation between a product tree and the list of its
leaves traversed left-to-right.
›