Theory Matrix_Peano_Algebras
section ‹Matrix Peano Algebras›
text ‹
We define a Boolean matrix representation of natural numbers up to ‹n›, where ‹n› the size of an enumeration type ‹'a::enum›.
Numbers (obtained by ‹Z_matrix› for ‹0› and ‹N_matrix n› for ‹n›) are represented as relational vectors.
The total successor function (‹S_matrix›, modulo ‹n›) and the partial successor function (‹S'_matrix›, for numbers up to ‹n-1›) are relations that are (partial) functions.
We give an order-embedding of ‹nat› into this representation.
We show that this representation satisfies a relational version of the Peano axioms.
We also implement a function ‹CP_matrix› that chooses a number in a non-empty set.
›
theory Matrix_Peano_Algebras
imports Aggregation_Algebras.M_Choose_Component Relational_Disjoint_Set_Forests.More_Disjoint_Set_Forests
begin
no_notation minus_class.minus (infixl ‹-› 65)
definition Z_matrix :: "('a::enum,'b::{bot,top}) square" (‹mZero›) where "mZero = (λ(i,j) . if i = hd enum_class.enum then top else bot)"
definition S_matrix :: "('a::enum,'b::{bot,top}) square" (‹msuccmod›) where "msuccmod = (λ(i,j) . let e = (enum_class.enum :: 'a list) in if (∃k . Suc k<length e ∧ i = e ! k ∧ j = e ! Suc k) ∨ (i = e ! minus_class.minus (length e) 1 ∧ j = hd e) then top else bot)"
definition S'_matrix :: "('a::enum,'b::{bot,top}) square" (‹msucc›) where "msucc = (λ(i,j) . let e = (enum_class.enum :: 'a list) in if ∃k . Suc k<length e ∧ i = e ! k ∧ j = e ! Suc k then top else bot)"
definition N_matrix :: "nat ⇒ ('a::enum,'b::{bot,top}) square" (‹mnat›) where "mnat n = (λ(i,j) . if i = enum_class.enum ! n then top else bot)"
definition CP_matrix :: "('a::enum,'b::{bot,uminus}) square ⇒ ('a,'b) square" (‹mcp›) where "mcp f = (λ(i,j) . if Some i = find (λx . f (x,x) ≠ bot) enum_class.enum then uminus_class.uminus (uminus_class.uminus (f (i,j))) else bot)"
lemma S'_matrix_S_matrix:
"(msucc :: ('a::enum,'b::stone_relation_algebra) square) = msuccmod ⊖ mZero⇧t"
proof (rule ext, rule prod_cases)
let ?e = "enum_class.enum :: 'a list"
let ?h = "hd ?e"
let ?s = "msuccmod :: ('a,'b) square"
let ?s' = "msucc :: ('a,'b) square"
let ?z = "mZero :: ('a,'b) square"
fix i j
have "?s' (i,j) = ?s (i,j) - ?z (j,i)"
proof (cases "j = ?h")
case True
have "?s' (i,j) = bot"
proof (unfold S'_matrix_def, clarsimp)
fix k
assume 1: "Suc k < length ?e" "j = ?e ! Suc k"
have "(UNIV :: 'a set) ≠ {}"
by simp
hence "?e ! Suc k = ?e ! 0"
using 1 by (simp add: hd_conv_nth UNIV_enum True)
hence "Suc k = 0"
apply (subst nth_eq_iff_index_eq[THEN sym, of ?e])
using 1 enum_distinct by auto
thus "top = bot"
by simp
qed
thus ?thesis
by (simp add: Z_matrix_def True)
next
case False
thus ?thesis
by (simp add: Z_matrix_def S_matrix_def S'_matrix_def)
qed
thus "?s' (i,j) = (?s ⊖ ?z⇧t) (i,j)"
by (simp add: minus_matrix_def conv_matrix_def Z_matrix_def)
qed
lemma N_matrix_power_S:
"n < length (enum_class.enum :: 'a list) ⟶ mnat n = matrix_monoid.power (msuccmod⇧t) n ⊙ (mZero :: ('a::enum,'b::stone_relation_algebra) square)"
proof (induct n)
let ?z = "mZero :: ('a,'b) square"
let ?s = "msuccmod :: ('a,'b) square"
let ?e = "enum_class.enum :: 'a list"
let ?h = "hd ?e"
let ?l = "length ?e"
let ?g = "?e ! minus_class.minus ?l 1"
let ?p = "matrix_monoid.power (?s⇧t)"
case 0
have "(UNIV :: 'a set) ≠ {}"
by simp
hence "?h = ?e ! 0"
by (simp add: hd_conv_nth UNIV_enum)
thus ?case
by (simp add: N_matrix_def Z_matrix_def)
case (Suc n)
assume 1: "n < ?l ⟶ mnat n = ?p n ⊙ ?z"
show "Suc n < ?l ⟶ mnat (Suc n) = ?p (Suc n) ⊙ ?z"
proof
assume 2: "Suc n < ?l"
hence "n < ?l"
by simp
hence "∀l<?l . (?e ! l = ?e ! n ⟶ l = n)"
using nth_eq_iff_index_eq enum_distinct by auto
hence 3: "⋀i . (∃l<?l . ?e ! n = ?e ! l ∧ i = ?e ! Suc l) ⟶ (i = ?e ! Suc n)"
by auto
have 4: "⋀i . (∃l . Suc l<?l ∧ ?e ! n = ?e ! l ∧ i = ?e ! Suc l) ⟷ (i = ?e ! Suc n)"
apply (rule iffI)
using 3 apply (metis Suc_lessD)
using 2 by auto
show "mnat (Suc n) = ?p (Suc n) ⊙ ?z"
proof (rule ext, rule prod_cases)
fix i j :: 'a
have "(?p (Suc n) ⊙ ?z) (i,j) = (?s⇧t ⊙ mnat n) (i,j)"
using 1 2 by (simp add: matrix_monoid.mult_assoc)
also have "... = (⨆⇩k ((?s (k,i))⇧T * mnat n (k,j)))"
by (simp add: times_matrix_def conv_matrix_def)
also have "... = (⨆⇩k ((if (∃l . Suc l<length ?e ∧ k = ?e ! l ∧ i = ?e ! Suc l) ∨ (k = ?g ∧ i = ?h) then top else bot)⇧T * (if k = ?e ! n then top else bot)))"
by (simp add: S_matrix_def N_matrix_def)
also have "... = (⨆⇩k ((if (∃l . Suc l<length ?e ∧ k = ?e ! l ∧ i = ?e ! Suc l) ∨ (k = ?g ∧ i = ?h) then top else bot) * (if k = ?e ! n then top else bot)))"
by (smt (verit, best) sup_monoid.sum.cong symmetric_bot_closed symmetric_top_closed)
also have "... = (⨆⇩k (if (∃l . Suc l<length ?e ∧ k = ?e ! l ∧ i = ?e ! Suc l ∧ k = ?e ! n) ∨ (k = ?g ∧ i = ?h ∧ k = ?e ! n) then top else bot))"
by (smt (verit, best) covector_bot_closed idempotent_bot_closed sup_monoid.sum.cong surjective_top_closed vector_bot_closed)
also have "... = (if ∃l . Suc l<length ?e ∧ ?e ! n = ?e ! l ∧ i = ?e ! Suc l then top else bot)"
proof -
have "⋀k . ¬(k = ?g ∧ i = ?h ∧ k = ?e ! n)"
using 2 distinct_conv_nth[of ?e] enum_distinct by auto
thus ?thesis
by (smt (verit, del_insts) comp_inf.ub_sum sup.order_iff sup_monoid.sum.neutral sup_top_right)
qed
also have "... = (if i = ?e ! Suc n then top else bot)"
using 4 by simp
also have "... = mnat (Suc n) (i,j)"
by (simp add: N_matrix_def)
finally show "mnat (Suc n) (i,j) = (?p (Suc n) ⊙ ?z) (i,j)"
by simp
qed
qed
qed
lemma N_matrix_power_S':
"n < length (enum_class.enum :: 'a list) ⟶ mnat n = matrix_monoid.power (msucc⇧t) n ⊙ (mZero :: ('a::enum,'b::stone_relation_algebra) square)"
proof (induct n)
let ?z = "mZero :: ('a,'b) square"
let ?s = "msucc :: ('a,'b) square"
let ?e = "enum_class.enum :: 'a list"
let ?h = "hd ?e"
let ?l = "length ?e"
let ?p = "matrix_monoid.power (?s⇧t)"
case 0
have "(UNIV :: 'a set) ≠ {}"
by simp
hence "?h = ?e ! 0"
by (simp add: hd_conv_nth UNIV_enum)
thus ?case
by (simp add: N_matrix_def Z_matrix_def)
case (Suc n)
assume 1: "n < ?l ⟶ mnat n = ?p n ⊙ ?z"
show "Suc n < ?l ⟶ mnat (Suc n) = ?p (Suc n) ⊙ ?z"
proof
assume 2: "Suc n < ?l"
hence "n < ?l"
by simp
hence "∀l<?l . (?e ! l = ?e ! n ⟶ l = n)"
using nth_eq_iff_index_eq enum_distinct by auto
hence 3: "⋀i . (∃l<?l . ?e ! n = ?e ! l ∧ i = ?e ! Suc l) ⟶ (i = ?e ! Suc n)"
by auto
have 4: "⋀i . (∃l . Suc l<?l ∧ ?e ! n = ?e ! l ∧ i = ?e ! Suc l) ⟷ (i = ?e ! Suc n)"
apply (rule iffI)
using 3 apply (metis Suc_lessD)
using 2 by auto
show "mnat (Suc n) = ?p (Suc n) ⊙ ?z"
proof (rule ext, rule prod_cases)
fix i j :: 'a
have "(?p (Suc n) ⊙ ?z) (i,j) = (?s⇧t ⊙ mnat n) (i,j)"
using 1 2 by (simp add: matrix_monoid.mult_assoc)
also have "... = (⨆⇩k ((?s (k,i))⇧T * mnat n (k,j)))"
by (simp add: times_matrix_def conv_matrix_def)
also have "... = (⨆⇩k ((if ∃l . Suc l<length ?e ∧ k = ?e ! l ∧ i = ?e ! Suc l then top else bot)⇧T * (if k = ?e ! n then top else bot)))"
by (simp add: S'_matrix_def N_matrix_def)
also have "... = (⨆⇩k ((if ∃l . Suc l<length ?e ∧ k = ?e ! l ∧ i = ?e ! Suc l then top else bot) * (if k = ?e ! n then top else bot)))"
by (smt (verit, best) sup_monoid.sum.cong symmetric_bot_closed symmetric_top_closed)
also have "... = (⨆⇩k (if ∃l . Suc l<length ?e ∧ k = ?e ! l ∧ i = ?e ! Suc l ∧ k = ?e ! n then top else bot))"
by (smt (verit, best) covector_bot_closed idempotent_bot_closed sup_monoid.sum.cong surjective_top_closed vector_bot_closed)
also have "... = (if ∃l . Suc l<length ?e ∧ ?e ! n = ?e ! l ∧ i = ?e ! Suc l then top else bot)"
by (smt (verit, del_insts) comp_inf.ub_sum sup.order_iff sup_monoid.sum.neutral sup_top_right)
also have "... = (if i = ?e ! Suc n then top else bot)"
using 4 by simp
also have "... = mnat (Suc n) (i,j)"
by (simp add: N_matrix_def)
finally show "mnat (Suc n) (i,j) = (?p (Suc n) ⊙ ?z) (i,j)"
by simp
qed
qed
qed
lemma N_matrix_power_S'_hom_zero:
"mnat 0 = (mZero :: ('a::enum,'b::stone_relation_algebra) square)"
proof -
let ?e = "enum_class.enum :: 'a list"
have "(UNIV :: 'a set) = set ?e"
using UNIV_enum by simp
hence "0 < length ?e"
by auto
thus ?thesis
using N_matrix_power_S' by force
qed
lemma N_matrix_power_S'_hom_succ:
assumes "Suc n < length (enum_class.enum :: 'a list)"
shows "mnat (Suc n) = msucc⇧t ⊙ (mnat n :: ('a::enum,'b::stone_relation_algebra) square)"
proof -
let ?e = "enum_class.enum :: 'a list"
let ?z = "mZero :: ('a,'b) square"
have 1: "n < length ?e"
using assms by simp
have "mnat (Suc n) = matrix_monoid.power (msucc⇧t) (Suc n) ⊙ ?z"
using assms N_matrix_power_S' by blast
also have "... = msucc⇧t ⊙ matrix_monoid.power (msucc⇧t) n ⊙ ?z"
by simp
also have "... = msucc⇧t ⊙ (matrix_monoid.power (msucc⇧t) n ⊙ ?z)"
by (simp add: matrix_monoid.mult_assoc)
also have "... = msucc⇧t ⊙ mnat n"
using 1 by (metis N_matrix_power_S')
finally show ?thesis
.
qed
lemma N_matrix_power_S'_hom_inj:
assumes "m < length (enum_class.enum :: 'a list)"
and "n < length (enum_class.enum :: 'a list)"
and "m ≠ n"
shows "mnat m ≠ (mnat n :: ('a::enum,'b::stone_relation_algebra_consistent) square)"
proof -
let ?e = "enum_class.enum :: 'a list"
let ?m = "?e ! m"
have 1: "mnat m (?m,?m) = top"
by (simp add: N_matrix_def)
have "mnat n (?m,?m) = bot"
apply (unfold N_matrix_def)
using assms enum_distinct nth_eq_iff_index_eq by auto
thus ?thesis
using 1 by (metis consistent)
qed
syntax
"_sum_sup_monoid" :: "idt ⇒ nat ⇒ 'a::bounded_semilattice_sup_bot ⇒ 'a" (‹(⨆_<_ . _)› [0,51,10] 10)
syntax_consts
"_sum_sup_monoid" == sup_monoid.sum
translations
"⨆x<y . t" => "XCONST sup_monoid.sum (λx . t) { x . x < y }"
context bounded_semilattice_sup_bot
begin
lemma ub_sum_nat:
fixes f :: "nat ⇒ 'a"
assumes "i < l"
shows "f i ≤ (⨆k<l . f k)"
by (metis (no_types, lifting) assms finite_Collect_less_nat sup_ge1 sup_monoid.sum.remove mem_Collect_eq)
lemma lub_sum_nat:
fixes f :: "nat ⇒ 'a"
assumes "∀k<l . f k ≤ x"
shows "(⨆k<l . f k) ≤ x"
apply (rule finite_subset_induct[where A="{k . k < l}"])
by (simp_all add: assms)
end
lemma ext_sum_nat:
fixes l :: nat
shows "(⨆k<l . f k x) = (⨆k<l . f k) x"
apply (rule finite_subset_induct[where A="{k . k < l}"])
apply simp
apply simp
apply (metis (no_types, lifting) bot_apply sup_monoid.sum.empty)
by (metis (mono_tags, lifting) sup_apply sup_monoid.sum.insert)