Theory Function_Ring
theory Function_Ring
imports "HOL-Algebra.Ring" "HOL-Library.FuncSet" "HOL-Algebra.Module"
begin
text‹
This theory formalizes basic facts about the ring of extensional functions from a fixed set to
a fixed ring. This will be useful for providing a generic framework for various constructions
related to the $p$-adics such as polynomial evaluation and sequences. The rings of semialgebraic
functions will be defined as subrings of these function rings, which will be necessary for the
proof of $p$-adic quantifier elimination.
›
section‹The Ring of Extensional Functions from a Fixed Base Set to a Fixed Base Ring›
subsection‹Basic Operations on Extensional Functions›
definition function_mult:: "'c set ⇒ ('a, 'b) ring_scheme ⇒ ('c ⇒ 'a) ⇒ ('c ⇒ 'a) ⇒ ('c ⇒ 'a)" where
"function_mult S R f g = (λx ∈ S. (f x) ⊗⇘R⇙ (g x))"
abbreviation(input) ring_function_mult:: "('a, 'b) ring_scheme ⇒ ('a ⇒ 'a) ⇒ ('a ⇒ 'a) ⇒ ('a ⇒ 'a)" where
"ring_function_mult R f g ≡ function_mult (carrier R) R f g"
definition function_add:: "'c set ⇒ ('a, 'b) ring_scheme ⇒ ('c ⇒ 'a) ⇒ ('c ⇒ 'a) ⇒ ('c ⇒ 'a)" where
"function_add S R f g = (λx ∈ S. (f x) ⊕⇘R⇙ (g x))"
abbreviation(input) ring_function_add:: "('a, 'b) ring_scheme ⇒ ('a ⇒ 'a) ⇒ ('a ⇒ 'a) ⇒ ('a ⇒ 'a)" where
"ring_function_add R f g ≡ function_add (carrier R) R f g"
definition function_one:: "'c set ⇒ ('a, 'b) ring_scheme ⇒ ('c ⇒ 'a)" where
"function_one S R = (λx ∈ S. 𝟭⇘R⇙)"
abbreviation(input) ring_function_one :: "('a, 'b) ring_scheme ⇒ ('a ⇒ 'a)" where
"ring_function_one R ≡ function_one (carrier R) R"
definition function_zero:: "'c set ⇒ ('a, 'b) ring_scheme ⇒ ('c ⇒ 'a)" where
"function_zero S R = (λx ∈ S. 𝟬⇘R⇙)"
abbreviation(input) ring_function_zero :: "('a, 'b) ring_scheme ⇒ ('a ⇒ 'a)" where
"ring_function_zero R ≡ function_zero (carrier R) R"
definition function_uminus:: "'c set ⇒ ('a, 'b) ring_scheme ⇒ ('c ⇒ 'a) ⇒ ('c ⇒ 'a)" where
"function_uminus S R a = (λ x ∈ S. ⊖⇘R⇙ (a x))"
definition ring_function_uminus:: " ('a, 'b) ring_scheme ⇒ ('a ⇒ 'a) ⇒ ('a ⇒ 'a)" where
"ring_function_uminus R a = function_uminus (carrier R) R a"
definition function_scalar_mult:: "'c set ⇒ ('a, 'b) ring_scheme ⇒ 'a ⇒ ('c ⇒ 'a) ⇒ ('c ⇒ 'a)" where
"function_scalar_mult S R a f = (λ x ∈ S. a ⊗⇘R⇙ (f x))"
subsection‹Defining the Ring of Extensional Functions›
definition function_ring:: "'c set ⇒ ('a, 'b) ring_scheme ⇒ ( 'a, 'c ⇒ 'a) module" where
"function_ring S R = ⦇
carrier = extensional_funcset S (carrier R),
Group.monoid.mult = (function_mult S R),
one = (function_one S R),
zero = (function_zero S R),
add = (function_add S R),
smult = function_scalar_mult S R ⦈ "
text‹The following locale consists of a struct R, and a distinguished set S which is meant to serve as the domain for a ring of functions $S \to carrier R$. ›
locale struct_functions =
fixes R ::"('a, 'b) partial_object_scheme" (structure)
and S :: "'c set"
text‹The following are locales which fix a ring R (which may be commutative, a domain, or a field) and a function ring F of extensional functions from a fixed set S to $carrier R$›
locale ring_functions = struct_functions + R?: ring R +
fixes F (structure)
defines F_def: "F ≡ function_ring S R"
locale cring_functions = ring_functions + R?: cring R
locale domain_functions = ring_functions + R?: domain R
locale field_functions = ring_functions + R?: field R
sublocale cring_functions < ring_functions
apply (simp add: ring_functions_axioms)
by (simp add: F_def)
sublocale domain_functions < ring_functions
apply (simp add: ring_functions_axioms)
by (simp add: F_def)
sublocale domain_functions < cring_functions
apply (simp add: cring_functions_def is_cring ring_functions_axioms)
by (simp add: F_def)
sublocale field_functions < domain_functions
apply (simp add: domain_axioms domain_functions_def ring_functions_axioms)
by (simp add: F_def)
sublocale field_functions < ring_functions
apply (simp add: ring_functions_axioms)
by (simp add: F_def)
sublocale field_functions < cring_functions
apply (simp add: cring_functions_axioms)
by (simp add: F_def)
abbreviation(input) ring_function_ring:: "('a, 'b) ring_scheme ⇒ ('a, 'a ⇒ 'a) module" (‹Fun›) where
"ring_function_ring R ≡ function_ring (carrier R) R"
subsection‹Algebraic Properties of the Basic Operations›
subsubsection‹Basic Carrier Facts›
lemma(in ring_functions) function_ring_defs:
"carrier F = extensional_funcset S (carrier R)"
"(⊗⇘F⇙) = (function_mult S R)"
"(⊕⇘F⇙) = (function_add S R)"
"𝟭⇘F⇙ = function_one S R"
"𝟬⇘F⇙ = function_zero S R"
"(⊙⇘F⇙) = function_scalar_mult S R"
unfolding F_def
by ( auto simp add: function_ring_def)
lemma(in ring_functions) function_ring_car_memE:
assumes "a ∈ carrier F"
shows "a ∈ extensional S"
"a ∈ S → carrier R"
using assms function_ring_defs apply auto[1]
using assms function_ring_defs PiE_iff apply blast
using assms function_ring_defs(1) by fastforce
lemma(in ring_functions) function_ring_car_closed:
assumes "a ∈ S"
assumes "f ∈ carrier F"
shows "f a ∈ carrier R"
using assms unfolding function_ring_def F_def by auto
lemma(in ring_functions) function_ring_not_car:
assumes "a ∉ S"
assumes "f ∈ carrier F"
shows "f a = undefined"
using assms unfolding function_ring_def F_def by auto
lemma(in ring_functions) function_ring_car_eqI:
assumes "f ∈ carrier F"
assumes "g ∈ carrier F"
assumes "⋀a. a ∈ S ⟹ f a = g a"
shows "f = g"
using assms(1) assms(2) assms(3) extensionalityI function_ring_car_memE(1) by blast
lemma(in ring_functions) function_ring_car_memI:
assumes "⋀a. a ∈ S ⟹ f a ∈ carrier R"
assumes "⋀ a. a ∉ S⟹ f a = undefined"
shows "f ∈ carrier F"
using function_ring_defs assms
unfolding extensional_funcset_def
by (simp add: ‹⋀a. a ∈ S ⟹ f a ∈ carrier R› extensional_def)
lemma(in ring) function_ring_car_memI:
assumes "⋀a. a ∈ S ⟹ f a ∈ carrier R"
assumes "⋀ a. a ∉ S⟹ f a = undefined"
shows "f ∈ carrier (function_ring S R)"
by (simp add: assms(1) assms(2) local.ring_axioms ring_functions.function_ring_car_memI ring_functions.intro)
subsubsection‹Basic Multiplication Facts›
lemma(in ring_functions) function_mult_eval_car:
assumes "a ∈ S"
assumes "f ∈ carrier F"
assumes "g ∈ carrier F"
shows "(f ⊗⇘F⇙ g) a = (f a) ⊗ (g a)"
using assms function_ring_defs
unfolding function_mult_def
by simp
lemma(in ring_functions) function_mult_eval_closed:
assumes "a ∈ S"
assumes "f ∈ carrier F"
assumes "g ∈ carrier F"
shows "(f ⊗⇘F⇙ g) a ∈ carrier R"
using assms function_mult_eval_car
using F_def ring_functions.function_ring_car_closed ring_functions_axioms by fastforce
lemma(in ring_functions) fun_mult_closed:
assumes "f ∈ carrier F"
assumes "g ∈ carrier F"
shows "f ⊗⇘F⇙ g ∈ carrier F"
apply(rule function_ring_car_memI)
apply (simp add: assms(1) assms(2) function_mult_eval_closed)
by (simp add: function_mult_def function_ring_defs(2))
lemma(in ring_functions) fun_mult_eval_assoc:
assumes "x ∈ carrier F"
assumes "y ∈ carrier F"
assumes " z ∈ carrier F"
assumes "a ∈ S"
shows "(x ⊗⇘F⇙ y ⊗⇘F⇙ z) a = (x ⊗⇘F⇙ (y ⊗⇘F⇙ z)) a"
proof-
have 0: "(x ⊗⇘F⇙ y ⊗⇘F⇙ z) a = (x a) ⊗ (y a) ⊗ (z a) "
by (simp add: assms(1) assms(2) assms(3) assms(4) fun_mult_closed function_mult_eval_car)
have 1: "(x ⊗⇘F⇙ (y ⊗⇘F⇙ z)) a = (x a) ⊗ ((y a) ⊗ (z a))"
by (simp add: assms(1) assms(2) assms(3) assms(4) fun_mult_closed function_mult_eval_car)
have 2:"(x ⊗⇘F⇙ (y ⊗⇘F⇙ z)) a = (x a) ⊗ (y a) ⊗ (z a)"
using 1 assms
by (simp add: function_ring_car_closed m_assoc)
show ?thesis
using 0 2 by auto
qed
lemma(in ring_functions) fun_mult_assoc:
assumes "x ∈ carrier F"
assumes "y ∈ carrier F"
assumes "z ∈ carrier F"
shows "(x ⊗⇘F⇙ y ⊗⇘F⇙ z) = (x ⊗⇘F⇙ (y ⊗⇘F⇙ z))"
using fun_mult_eval_assoc[of x]
by (simp add: assms(1) assms(2) assms(3) fun_mult_closed function_ring_car_eqI)
subsubsection‹Basic Addition Facts›
lemma(in ring_functions) fun_add_eval_car:
assumes "a ∈ S"
assumes "f ∈ carrier F"
assumes "g ∈ carrier F"
shows "(f ⊕⇘F⇙ g) a = (f a) ⊕ (g a)"
by (simp add: assms(1) function_add_def function_ring_defs(3))
lemma(in ring_functions) fun_add_eval_closed:
assumes "a ∈ S"
assumes "f ∈ carrier F"
assumes "g ∈ carrier F"
shows "(f ⊕⇘F⇙ g) a ∈ carrier R"
using assms unfolding F_def
using F_def fun_add_eval_car function_ring_car_closed
by auto
lemma(in ring_functions) fun_add_closed:
assumes "f ∈ carrier F"
assumes "g ∈ carrier F"
shows "f ⊕⇘F⇙ g ∈ carrier F"
apply(rule function_ring_car_memI)
using assms unfolding F_def
using F_def fun_add_eval_closed apply blast
by (simp add: function_add_def function_ring_def)
lemma(in ring_functions) fun_add_eval_assoc:
assumes "x ∈ carrier F"
assumes "y ∈ carrier F"
assumes " z ∈ carrier F"
assumes "a ∈ S"
shows "(x ⊕⇘F⇙ y ⊕⇘F⇙ z) a = (x ⊕⇘F⇙ (y ⊕⇘F⇙ z)) a"
proof-
have 0: "(x ⊕⇘F⇙ y ⊕⇘F⇙ z) a = (x a) ⊕ (y a) ⊕ (z a) "
by (simp add: assms(1) assms(2) assms(3) assms(4) fun_add_closed fun_add_eval_car)
have 1: "(x ⊕⇘F⇙ (y ⊕⇘F⇙ z)) a = (x a) ⊕ ((y a) ⊕ (z a))"
by (simp add: assms(1) assms(2) assms(3) assms(4) fun_add_closed fun_add_eval_car)
have 2:"(x ⊕⇘F⇙ (y ⊕⇘F⇙ z)) a = (x a) ⊕ (y a) ⊕ (z a)"
using 1 assms
by (simp add: add.m_assoc function_ring_car_closed)
show ?thesis
using 0 2 by auto
qed
lemma(in ring_functions) fun_add_assoc:
assumes "x ∈ carrier F"
assumes "y ∈ carrier F"
assumes " z ∈ carrier F"
shows "x ⊕⇘F⇙ y ⊕⇘F⇙ z = x ⊕⇘F⇙ (y ⊕⇘F⇙ z)"
apply(rule function_ring_car_eqI)
using assms apply (simp add: fun_add_closed)
apply (simp add: assms(1) assms(2) assms(3) fun_add_closed)
by (simp add: assms(1) assms(2) assms(3) fun_add_eval_assoc)
lemma(in ring_functions) fun_add_eval_comm:
assumes "a ∈ S"
assumes "x ∈ carrier F"
assumes "y ∈ carrier F"
shows "(x ⊕⇘F⇙ y) a = (y ⊕⇘F⇙ x) a"
by (metis F_def assms(1) assms(2) assms(3) fun_add_eval_car ring.ring_simprules(10) ring_functions.function_ring_car_closed ring_functions_axioms ring_functions_def)
lemma(in ring_functions) fun_add_comm:
assumes "x ∈ carrier F"
assumes "y ∈ carrier F"
shows "x ⊕⇘F⇙ y = y ⊕⇘F⇙ x"
using fun_add_eval_comm assms
by (metis (no_types, opaque_lifting) fun_add_closed function_ring_car_eqI)
subsubsection‹Basic Facts About the Multiplicative Unit›
lemma(in ring_functions) function_one_eval:
assumes "a ∈ S"
shows "𝟭⇘F⇙ a = 𝟭"
using assms function_ring_defs unfolding function_one_def
by simp
lemma(in ring_functions) function_one_closed:
"𝟭⇘F⇙ ∈carrier F"
apply(rule function_ring_car_memI)
using function_ring_defs
using function_one_eval apply auto[1]
by (simp add: function_one_def function_ring_defs(4))
lemma(in ring_functions) function_times_one_l:
assumes "a ∈ carrier F"
shows "𝟭⇘F⇙ ⊗⇘F⇙ a = a"
proof(rule function_ring_car_eqI)
show "𝟭⇘F⇙ ⊗⇘F⇙ a ∈ carrier F"
using assms fun_mult_closed function_one_closed
by blast
show " a ∈ carrier F"
using assms by simp
show "⋀c. c ∈ S ⟹ (𝟭⇘F⇙ ⊗⇘F⇙ a) c = a c "
by (simp add: assms function_mult_eval_car function_one_eval function_one_closed function_ring_car_closed)
qed
lemma(in ring_functions) function_times_one_r:
assumes "a ∈ carrier F"
shows "a⊗⇘F⇙ 𝟭⇘F⇙ = a"
proof(rule function_ring_car_eqI)
show "a⊗⇘F⇙ 𝟭⇘F⇙ ∈ carrier F"
using assms fun_mult_closed function_one_closed
by blast
show " a ∈ carrier F"
using assms by simp
show "⋀c. c ∈ S ⟹ (a⊗⇘F⇙ 𝟭⇘F⇙) c = a c "
using assms
by (simp add: function_mult_eval_car function_one_eval function_one_closed function_ring_car_closed)
qed
subsubsection‹Basic Facts About the Additive Unit›
lemma(in ring_functions) function_zero_eval:
assumes "a ∈ S"
shows "𝟬⇘F⇙ a = 𝟬"
using assms function_ring_defs
unfolding function_zero_def
by simp
lemma(in ring_functions) function_zero_closed:
"𝟬⇘F⇙ ∈carrier F"
apply(rule function_ring_car_memI)
apply (simp add: function_zero_eval)
by (simp add: function_ring_defs(5) function_zero_def)
lemma(in ring_functions) fun_add_zeroL:
assumes "a ∈ carrier F"
shows "𝟬⇘F⇙ ⊕⇘F⇙ a = a"
proof(rule function_ring_car_eqI)
show "𝟬⇘F⇙ ⊕⇘F⇙ a ∈ carrier F"
using assms fun_add_closed function_zero_closed
by blast
show "a ∈ carrier F"
using assms by simp
show "⋀c. c ∈ S ⟹ (𝟬⇘F⇙ ⊕⇘F⇙ a) c = a c "
using assms F_def fun_add_eval_car function_zero_closed
ring_functions.function_zero_eval ring_functions_axioms
by (simp add: ring_functions.function_zero_eval function_ring_car_closed)
qed
lemma(in ring_functions) fun_add_zeroR:
assumes "a ∈ carrier F"
shows "a ⊕⇘F⇙ 𝟬⇘F⇙ = a"
using assms fun_add_comm fun_add_zeroL
by (simp add: function_zero_closed)
subsubsection‹Distributive Laws›
lemma(in ring_functions) function_mult_r_distr:
assumes "x ∈ carrier F"
assumes" y ∈ carrier F"
assumes " z ∈ carrier F"
shows " (x ⊕⇘F⇙ y) ⊗⇘F⇙ z = x ⊗⇘F⇙ z ⊕⇘F⇙ y ⊗⇘F⇙ z"
proof(rule function_ring_car_eqI)
show "(x ⊕⇘F⇙ y) ⊗⇘F⇙ z ∈ carrier F"
by (simp add: assms(1) assms(2) assms(3) fun_add_closed fun_mult_closed)
show "x ⊗⇘F⇙ z ⊕⇘F⇙ y ⊗⇘F⇙ z ∈ carrier F"
by (simp add: assms(1) assms(2) assms(3) fun_add_closed fun_mult_closed)
show "⋀a. a ∈ S ⟹ ((x ⊕⇘F⇙ y) ⊗⇘F⇙ z) a = (x ⊗⇘F⇙ z ⊕⇘F⇙ y ⊗⇘F⇙ z) a"
proof-
fix a
assume A: "a ∈ S"
show "((x ⊕⇘F⇙ y) ⊗⇘F⇙ z) a = (x ⊗⇘F⇙ z ⊕⇘F⇙ y ⊗⇘F⇙ z) a"
using A assms fun_add_eval_car[of a x y] fun_add_eval_car[of a "x ⊗⇘F⇙z" "y ⊗⇘F⇙ z"]
function_mult_eval_car[of a "x ⊕⇘F⇙ y" z] semiring_simprules(10)
F_def
by (smt (verit) fun_add_closed function_mult_eval_car function_ring_car_closed
ring_functions.fun_mult_closed ring_functions_axioms)
qed
qed
lemma(in ring_functions) function_mult_l_distr:
assumes "x ∈ carrier F"
assumes" y ∈ carrier F"
assumes " z ∈ carrier F"
shows "z ⊗⇘F⇙ (x ⊕⇘F⇙ y) = z ⊗⇘F⇙ x ⊕⇘F⇙ z ⊗⇘F⇙ y"
proof(rule function_ring_car_eqI)
show "z ⊗⇘F⇙ (x ⊕⇘F⇙ y) ∈ carrier F"
by (simp add: assms(1) assms(2) assms(3) fun_add_closed fun_mult_closed)
show "z ⊗⇘F⇙ x ⊕⇘F⇙ z ⊗⇘F⇙ y ∈ carrier F"
by (simp add: assms(1) assms(2) assms(3) fun_add_closed fun_mult_closed)
show "⋀a. a ∈ S ⟹ (z ⊗⇘F⇙ (x ⊕⇘F⇙ y)) a = (z ⊗⇘F⇙ x ⊕⇘F⇙ z ⊗⇘F⇙ y) a"
proof-
fix a
assume A: "a ∈ S"
show "(z ⊗⇘F⇙ (x ⊕⇘F⇙ y)) a = (z ⊗⇘F⇙ x ⊕⇘F⇙ z ⊗⇘F⇙ y) a"
using A assms function_ring_defs fun_add_closed fun_mult_closed
function_mult_eval_car[of a z "x ⊕⇘F⇙ y"]
function_mult_eval_car[of a z x]
function_mult_eval_car[of a z y]
fun_add_eval_car[of a x y]
semiring_simprules(13)
fun_add_eval_car function_ring_car_closed by auto
qed
qed
subsubsection‹Additive Inverses›
lemma(in ring_functions) function_uminus_closed:
assumes "f ∈ carrier F"
shows "function_uminus S R f ∈ carrier F"
proof(rule function_ring_car_memI)
show "⋀a. a ∈ S ⟹ function_uminus S R f a ∈ carrier R"
using assms function_ring_car_closed[of _ f] unfolding function_uminus_def
by simp
show "⋀a. a ∉ S ⟹ function_uminus S R f a = undefined"
by (simp add: function_uminus_def)
qed
lemma(in ring_functions) function_uminus_eval:
assumes "a ∈ S"
assumes "f ∈ carrier F"
shows "(function_uminus S R f) a = ⊖ (f a)"
using assms unfolding function_uminus_def
by simp
lemma(in ring_functions) function_uminus_add_r:
assumes "a ∈ S"
assumes "f ∈ carrier F"
shows "f ⊕⇘F⇙ function_uminus S R f = 𝟬⇘F⇙"
apply(rule function_ring_car_eqI)
using assms fun_add_closed function_uminus_closed apply blast
unfolding F_def using F_def function_zero_closed apply blast
using F_def assms(2) fun_add_eval_car function_ring_car_closed function_uminus_closed
function_uminus_eval function_zero_eval r_neg by auto
lemma(in ring_functions) function_uminus_add_l:
assumes "a ∈ S"
assumes "f ∈ carrier F"
shows "function_uminus S R f ⊕⇘F⇙ f = 𝟬⇘F⇙"
using assms(1) assms(2) fun_add_comm function_uminus_add_r function_uminus_closed by auto
subsubsection‹Scalar Multiplication›
lemma(in ring_functions) function_smult_eval:
assumes "a ∈ carrier R"
assumes "f ∈ carrier F"
assumes "b ∈ S"
shows "(a ⊙⇘F⇙ f) b = a ⊗ (f b)"
using function_ring_defs(6) unfolding function_scalar_mult_def
by(simp add: assms)
lemma(in ring_functions) function_smult_closed:
assumes "a ∈ carrier R"
assumes "f ∈ carrier F"
shows "a ⊙⇘F⇙ f ∈ carrier F"
apply(rule function_ring_car_memI)
using function_smult_eval assms
apply (simp add: function_ring_car_closed)
using function_scalar_mult_def F_def
by (metis function_ring_defs(6) restrict_apply)
lemma(in ring_functions) function_smult_assoc1:
assumes "a ∈ carrier R"
assumes "b ∈ carrier R"
assumes "f ∈ carrier F"
shows "b ⊙⇘F⇙ (a ⊙⇘F⇙ f) = (b ⊗ a)⊙⇘F⇙f"
apply(rule function_ring_car_eqI)
using assms function_smult_closed apply simp
using assms function_smult_closed apply simp
by (metis F_def assms(1) assms(2) assms(3) function_mult_eval_closed function_one_closed
function_smult_eval function_times_one_r m_assoc m_closed ring_functions.function_smult_closed ring_functions_axioms)
lemma(in ring_functions) function_smult_assoc2:
assumes "a ∈ carrier R"
assumes "f ∈ carrier F"
assumes "g ∈ carrier F"
shows "(a ⊙⇘F⇙ f)⊗⇘F⇙g = a ⊙⇘F⇙ (f ⊗⇘F⇙ g)"
apply(rule function_ring_car_eqI)
using assms function_smult_closed apply (simp add: fun_mult_closed)
apply (simp add: assms(1) assms(2) assms(3) fun_mult_closed function_smult_closed)
by (metis (full_types) F_def assms(1) assms(2) assms(3) fun_mult_closed
function_mult_eval_car function_smult_closed function_smult_eval m_assoc ring_functions.function_ring_car_closed ring_functions_axioms)
lemma(in ring_functions) function_smult_one:
assumes "f ∈ carrier F"
shows "𝟭⊙⇘F⇙f = f"
apply(rule function_ring_car_eqI)
apply (simp add: assms function_smult_closed)
apply (simp add: assms)
by (simp add: assms function_ring_car_closed function_smult_eval)
lemma(in ring_functions) function_smult_l_distr:
"[| a ∈ carrier R; b ∈ carrier R; x ∈ carrier F |] ==>
(a ⊕ b) ⊙⇘F⇙ x = a ⊙⇘F⇙ x ⊕⇘F⇙ b ⊙⇘F⇙ x"
apply(rule function_ring_car_eqI)
apply (simp add: function_smult_closed)
apply (simp add: fun_add_closed function_smult_closed)
using function_smult_eval
by (simp add: fun_add_eval_car function_ring_car_closed function_smult_closed l_distr)
lemma(in ring_functions) function_smult_r_distr:
"[| a ∈ carrier R; x ∈ carrier F; y ∈ carrier F |] ==>
a ⊙⇘F⇙ (x ⊕⇘F⇙ y) = a ⊙⇘F⇙ x ⊕⇘F⇙ a ⊙⇘F⇙ y"
apply(rule function_ring_car_eqI)
apply (simp add: fun_add_closed function_smult_closed)
apply (simp add: fun_add_closed function_smult_closed)
by (simp add: fun_add_closed fun_add_eval_car function_ring_car_closed function_smult_closed function_smult_eval r_distr)
subsubsection‹The Ring of Functions Forms an Algebra›
lemma(in ring_functions) function_ring_is_abelian_group:
"abelian_group F"
apply(rule abelian_groupI)
apply (simp add: fun_add_closed)
apply (simp add: function_zero_closed)
using fun_add_assoc apply simp
apply (simp add: fun_add_comm)
apply (simp add: fun_add_comm fun_add_zeroR function_zero_closed)
using fun_add_zeroL function_ring_car_eqI function_uminus_add_l
function_uminus_closed function_zero_closed by blast
lemma(in ring_functions) function_ring_is_monoid:
"monoid F"
apply(rule monoidI)
apply (simp add: fun_mult_closed)
apply (simp add: function_one_closed)
apply (simp add: fun_mult_assoc)
apply (simp add: function_times_one_l)
by (simp add: function_times_one_r)
lemma(in ring_functions) function_ring_is_ring:
"ring F"
apply(rule ringI)
apply (simp add: function_ring_is_abelian_group)
apply (simp add: function_ring_is_monoid)
apply (simp add: function_mult_r_distr)
by (simp add: function_mult_l_distr)
sublocale ring_functions < F?: ring F
by (rule function_ring_is_ring)
lemma(in cring_functions) function_mult_comm:
assumes "x ∈ carrier F"
assumes" y ∈ carrier F"
shows "x ⊗⇘F⇙ y = y ⊗⇘F⇙ x"
apply(rule function_ring_car_eqI)
apply (simp add: assms(1) assms(2) fun_mult_closed)
apply (simp add: assms(1) assms(2) fun_mult_closed)
by (simp add: assms(1) assms(2) function_mult_eval_car function_ring_car_closed m_comm)
lemma(in cring_functions) function_ring_is_comm_monoid:
"comm_monoid F"
apply(rule comm_monoidI)
using fun_mult_assoc function_one_closed
apply (simp add: fun_mult_closed)
apply (simp add: function_one_closed)
apply (simp add: fun_mult_assoc)
apply (simp add: function_times_one_l)
by (simp add: function_mult_comm)
lemma(in cring_functions) function_ring_is_cring:
"cring F"
apply(rule cringI)
apply (simp add: function_ring_is_abelian_group)
apply (simp add: function_ring_is_comm_monoid)
by (simp add: function_mult_r_distr)
lemma(in cring_functions) function_ring_is_algebra:
"algebra R F"
apply(rule algebraI)
apply (simp add: is_cring)
apply (simp add: function_ring_is_cring)
using function_smult_closed apply blast
apply (simp add: function_smult_l_distr)
apply (simp add: function_smult_r_distr)
apply (simp add: function_smult_assoc1)
apply (simp add: function_smult_one)
by (simp add: function_smult_assoc2)
lemma(in ring_functions) function_uminus:
assumes "f ∈ carrier F"
shows "⊖⇘F⇙ f = (function_uminus S R) f"
using assms a_inv_def[of F]
by (metis F_def abelian_group.a_group abelian_group.r_neg function_uminus_add_r function_uminus_closed group.inv_closed partial_object.select_convs(1) ring.ring_simprules(18) ring_functions.function_ring_car_eqI ring_functions.function_ring_is_abelian_group ring_functions.function_ring_is_ring ring_functions_axioms)
lemma(in ring_functions) function_uminus_eval':
assumes "f ∈ carrier F"
assumes "a ∈ S"
shows "(⊖⇘F⇙ f) a = (function_uminus S R) f a"
using assms
by (simp add: function_uminus)
lemma(in ring_functions) function_uminus_eval'':
assumes "f ∈ carrier F"
assumes "a ∈ S"
shows "(⊖⇘F⇙ f) a = ⊖ (f a)"
using assms(1) assms(2) function_uminus
by (simp add: function_uminus_eval)
sublocale cring_functions < F?: algebra R F
using function_ring_is_algebra by auto
subsection‹Constant Functions›
definition constant_function where
"constant_function S a =(λx ∈ S. a)"
abbreviation(in ring_functions)(input) const where
"const ≡ constant_function S"
lemma(in ring_functions) constant_function_closed:
assumes "a ∈ carrier R"
shows "const a ∈ carrier F"
apply(rule function_ring_car_memI)
unfolding constant_function_def
apply (simp add: assms)
by simp
lemma(in ring_functions) constant_functionE:
assumes "a ∈ carrier R"
assumes "b ∈ S"
shows "const a b = a"
by (simp add: assms(2) constant_function_def)
lemma(in ring_functions) constant_function_add:
assumes "a ∈ carrier R"
assumes "b ∈ carrier R"
shows "const (a ⊕⇘R⇙ b) = (const a) ⊕⇘F⇙ (const b) "
apply(rule function_ring_car_eqI)
apply (simp add: constant_function_closed assms(1) assms(2))
using assms(1) constant_function_closed assms(2) fun_add_closed apply auto[1]
by (simp add: assms(1) assms(2) constant_function_closed constant_functionE fun_add_eval_car)
lemma(in ring_functions) constant_function_mult:
assumes "a ∈ carrier R"
assumes "b ∈ carrier R"
shows "const (a ⊗⇘R⇙ b) = (const a) ⊗⇘F⇙ (const b)"
apply(rule function_ring_car_eqI)
apply (simp add: constant_function_closed assms(1) assms(2))
using assms(1) constant_function_closed assms(2) fun_mult_closed apply auto[1]
by (simp add: constant_function_closed assms(1) assms(2) constant_functionE function_mult_eval_car)
lemma(in ring_functions) constant_function_minus:
assumes "a ∈ carrier R"
shows "⊖⇘F⇙(const a) = (const (⊖⇘R⇙ a)) "
apply(rule function_ring_car_eqI)
apply (simp add: constant_function_closed assms local.function_uminus)
apply (simp add: constant_function_closed assms function_uminus_closed)
apply (simp add: constant_function_closed assms)
by (simp add: constant_function_closed assms constant_functionE function_uminus_eval'')
lemma(in ring_functions) function_one_is_constant:
"const 𝟭 = 𝟭⇘F⇙"
unfolding F_def
apply(rule function_ring_car_eqI)
apply (simp add: constant_function_closed)
using F_def function_one_closed apply auto[1]
using F_def constant_functionE function_one_eval by auto
lemma(in ring_functions) function_zero_is_constant:
"const 𝟬 = 𝟬⇘F⇙"
apply(rule function_ring_car_eqI)
apply (simp add: constant_function_closed)
using F_def function_zero_closed apply auto[1]
using F_def constant_functionE function_zero_eval by auto
subsection‹Special Examples of Functions Rings›
subsubsection‹Functions from the Carrier of a Ring to Itself›
locale U_function_ring = ring
locale U_function_cring = U_function_ring + cring
sublocale U_function_ring < S?: struct_functions R "carrier R"
done
sublocale U_function_ring < FunR?: ring_functions R "carrier R" "Fun R"
apply (simp add: local.ring_axioms ring_functions.intro)
by simp
sublocale U_function_cring < FunR?: cring_functions R "carrier R" "Fun R"
apply (simp add: cring_functions_def is_cring ring_functions_axioms)
by simp
abbreviation(in U_function_ring)(input) ring_compose :: "('a ⇒ 'a) ⇒ ('a ⇒ 'a) ⇒ ('a ⇒ 'a)" where
"ring_compose ≡ compose (carrier R)"
lemma(in U_function_ring) ring_function_ring_comp:
assumes "f ∈ carrier (Fun R)"
assumes "g ∈ carrier (Fun R)"
shows "ring_compose f g ∈ carrier (Fun R)"
apply(rule function_ring_car_memI)
apply (simp add: assms(1) assms(2) compose_eq)
apply (simp add: assms(1) assms(2) function_ring_car_closed)
by (meson compose_extensional extensional_arb)
abbreviation(in U_function_ring)(input) ring_const (‹𝔠ı›) where
"ring_const ≡ constant_function (carrier R)"
lemma(in ring_functions) function_nat_pow_eval:
assumes "f ∈ carrier F"
assumes "s ∈ S"
shows "(f[^]⇘F⇙(n::nat)) s = (f s)[^]n"
apply(induction n)
using assms(2) function_one_eval apply auto[1]
by (simp add: assms(1) assms(2) function_mult_eval_car function_ring_is_monoid monoid.nat_pow_closed)
context U_function_ring
begin
definition a_translate :: "'a ⇒ 'a ⇒ 'a" where
"a_translate = (λ r ∈ carrier R. restrict ((add R) r) (carrier R))"
definition m_translate :: "'a ⇒ 'a ⇒ 'a" where
"m_translate = (λ r ∈ carrier R. restrict ((mult R) r) (carrier R))"
definition nat_power :: "nat ⇒ 'a ⇒ 'a" where
"nat_power = (λ(n::nat). restrict (λa. a[^]⇘R⇙n) (carrier R)) "
text‹Restricted operations are in Fs›
lemma a_translate_functions:
assumes "c ∈ carrier R"
shows "a_translate c ∈ carrier (Fun R)"
apply(rule function_ring_car_memI)
using assms a_translate_def
apply simp
using assms a_translate_def
by simp
lemma m_translate_functions:
assumes "c ∈ carrier R"
shows "m_translate c ∈ carrier (Fun R)"
apply(rule function_ring_car_memI)
using assms m_translate_def
apply simp
using assms m_translate_def
by simp
lemma nat_power_functions:
shows "nat_power n ∈ carrier (Fun R)"
apply(rule function_ring_car_memI)
using nat_power_def
apply simp
by (simp add: nat_power_def)
text‹Restricted operations simps›
lemma a_translate_eq:
assumes "c ∈ carrier R"
assumes "a ∈ carrier R"
shows "a_translate c a = c ⊕ a"
by (simp add: a_translate_def assms(1) assms(2))
lemma a_translate_eq':
assumes "c ∈ carrier R"
assumes "a ∉ carrier R"
shows "a_translate c a = undefined"
by (meson a_translate_functions assms(1) assms(2) function_ring_not_car)
lemma a_translate_eq'':
assumes "c ∉ carrier R"
shows "a_translate c = undefined"
by (simp add: a_translate_def assms)
lemma m_translate_eq:
assumes "c ∈ carrier R"
assumes "a ∈ carrier R"
shows "m_translate c a = c ⊗ a"
by (simp add: m_translate_def assms(1) assms(2))
lemma m_translate_eq':
assumes "c ∈ carrier R"
assumes "a ∉ carrier R"
shows "m_translate c a = undefined "
by (meson m_translate_functions assms(1) assms(2) function_ring_not_car)
lemma m_translate_eq'':
assumes "c ∉ carrier R"
shows "m_translate c = undefined"
by (simp add: m_translate_def assms)
lemma nat_power_eq:
assumes "a ∈ carrier R"
shows "nat_power n a = a[^]⇘R⇙ n"
by (simp add: assms nat_power_def)
lemma nat_power_eq':
assumes "a ∉ carrier R"
shows "nat_power n a = undefined"
by (simp add: assms nat_power_def)
text‹Constant ring\_function properties›
lemma constant_function_eq:
assumes "a ∈ carrier R"
assumes "b ∈ carrier R"
shows "𝔠⇘a⇙ b = a"
using assms
by (simp add: constant_functionE)
lemma constant_function_eq':
assumes "a ∈ carrier R"
assumes "b ∉ carrier R"
shows "𝔠⇘a⇙ b = undefined"
by (simp add: constant_function_closed assms(1) assms(2) function_ring_not_car)
text‹Compound expressions from algebraic operations›
end
definition monomial_function where
"monomial_function R c (n::nat) = (λ x ∈ carrier R. c ⊗⇘R⇙ (x[^]⇘R⇙n))"
context U_function_ring
begin
abbreviation monomial where
"monomial ≡ monomial_function R"
lemma monomial_functions:
assumes "c ∈ carrier R"
shows "monomial c n ∈ carrier (Fun R)"
apply(rule function_ring_car_memI)
unfolding monomial_function_def
apply (simp add: assms)
by simp
definition ring_id where
"ring_id ≡ restrict (λx. x) (carrier R) "
lemma ring_id_closed[simp]:
"ring_id ∈ carrier (Fun R)"
by (simp add: function_ring_car_memI ring_id_def)
lemma ring_id_eval:
assumes "a ∈ carrier R"
shows "ring_id a = a"
using assms unfolding ring_id_def
by simp
lemma constant_a_trans:
assumes "a ∈carrier R"
shows "m_translate a = 𝔠⇘a⇙ ⊗⇘Fun R⇙ ring_id"
proof(rule function_ring_car_eqI)
show "m_translate a ∈ carrier (Fun R)"
using assms
using m_translate_functions by blast
show "𝔠⇘a⇙ ⊗⇘Fun R⇙ ring_id ∈ carrier (Fun R)"
unfolding ring_id_def
using assms ring_id_closed ring_id_def
by (simp add: constant_function_closed fun_mult_closed)
show "⋀x. x ∈ carrier R ⟹ m_translate a x = (𝔠⇘a⇙ ⊗⇘Fun R⇙ ring_id) x"
by (simp add: constant_function_closed assms constant_function_eq function_mult_eval_car m_translate_eq ring_id_eval)
qed
text‹polynomials in one variable›
fun polynomial :: "'a list ⇒ ('a ⇒ 'a)" where
"polynomial [] = 𝟬⇘Fun R⇙ "|
"polynomial (a#as) = (λx ∈ carrier R. a ⊕ x ⊗ (polynomial as x))"
lemma polynomial_induct_lemma:
assumes "f ∈ carrier (Fun R)"
assumes "a ∈ carrier R"
shows "(λx ∈ carrier R. a ⊕ x ⊗ (f x)) ∈ carrier (Fun R)"
proof(rule function_ring_car_memI)
show "⋀aa. aa ∈ carrier R ⟹ (λx∈carrier R. a ⊕ x ⊗ f x) aa ∈ carrier R"
proof- fix y assume A: "y ∈ carrier R"
have "a ⊕ y ⊗ f y ∈ carrier R"
using A assms(1) assms(2) function_ring_car_closed by blast
thus "(λx∈carrier R. a ⊕ x ⊗ f x) y ∈ carrier R"
using A by auto
qed
show "⋀aa. aa ∉ carrier R ⟹ (λx∈carrier R. a ⊕ x ⊗ f x) aa = undefined"
by auto
qed
lemma polynomial_function:
shows "set as ⊆ carrier R ⟹ polynomial as ∈ carrier (Fun R)"
proof(induction as)
case Nil
then show ?case
by (simp add: function_zero_closed)
next
case (Cons a as)
then show "polynomial (a # as) ∈ carrier (function_ring (carrier R) R)"
using polynomial.simps(2)[of a as] polynomial_induct_lemma[of "polynomial as" a]
by simp
qed
lemma polynomial_constant:
assumes "a ∈ carrier R"
shows "polynomial [a] = 𝔠⇘a⇙"
apply(rule function_ring_car_eqI)
using assms polynomial_function
apply (metis (full_types) list.distinct(1) list.set_cases set_ConsD subset_code(1))
apply (simp add: constant_function_closed assms)
using polynomial.simps(2)[of a "[]"] polynomial.simps(1) assms
by (simp add: constant_function_eq function_zero_eval)
end
subsubsection‹Sequences Indexed by the Natural Numbers›
definition nat_seqs (‹_⇗ω⇖›)where
"nat_seqs R ≡ function_ring (UNIV::nat set) R"
abbreviation(input) closed_seqs where
"closed_seqs R ≡ carrier (R⇗ω⇖)"
lemma closed_seqs_memI:
assumes "⋀k. s k ∈ carrier R"
shows "s ∈ closed_seqs R"
unfolding nat_seqs_def function_ring_def
by (simp add: PiE_UNIV_domain assms)
lemma closed_seqs_memE:
assumes "s ∈ closed_seqs R"
shows "s k ∈ carrier R"
using assms unfolding nat_seqs_def function_ring_def
by (simp add: PiE_iff)
definition is_constant_fun where
"is_constant_fun R f = (∃x ∈ carrier R. f = constant_function (carrier R) R x)"
definition is_constant_seq where
"is_constant_seq R s = (∃x ∈ carrier R. s = constant_function (UNIV::nat set) x)"
lemma is_constant_seqI:
fixes a
assumes "s ∈ closed_seqs R"
assumes "⋀k. s k = a"
shows "is_constant_seq R s"
unfolding is_constant_seq_def constant_function_def
by (metis assms(1) assms(2) closed_seqs_memE restrict_UNIV restrict_ext)
lemma is_constant_seqE:
assumes "is_constant_seq R s"
assumes "s k = a"
shows "s n = a"
using assms unfolding is_constant_seq_def
by (metis constant_function_def restrict_UNIV)
lemma is_constant_seq_imp_closed:
assumes "is_constant_seq R s"
shows "s ∈ closed_seqs R"
apply(rule closed_seqs_memI)
using assms unfolding is_constant_seq_def constant_function_def
by auto
context U_function_ring
begin
text‹Sequence sums and products are closed›
lemma seq_plus_closed:
assumes "s ∈ closed_seqs R"
assumes "s' ∈ closed_seqs R"
shows "s ⊕⇘R⇗ω⇖⇙ s' ∈ closed_seqs R"
by (metis assms(1) assms(2) nat_seqs_def ring_functions.fun_add_closed ring_functions_axioms)
lemma seq_mult_closed:
assumes "s ∈ closed_seqs R"
assumes "s' ∈ closed_seqs R"
shows "s ⊗⇘R⇗ω⇖⇙ s' ∈ closed_seqs R"
apply(rule closed_seqs_memI)
by (metis assms(1) assms(2) closed_seqs_memE nat_seqs_def ring_functions.fun_mult_closed ring_functions_axioms)
lemma constant_function_comp_is_closed_seq:
assumes "a ∈ carrier R"
assumes "s ∈ closed_seqs R"
shows "(const a ∘ s) ∈ closed_seqs R"
by (simp add: constant_functionE assms(1) assms(2) closed_seqs_memE closed_seqs_memI)
lemma constant_function_comp_is_constant_seq:
assumes "a ∈ carrier R"
assumes "s ∈ closed_seqs R"
shows "is_constant_seq R ((const a) ∘ s)"
apply(rule is_constant_seqI[of _ _ a] )
apply (simp add: assms(1) assms(2) constant_function_comp_is_closed_seq)
using assms(1) assms(2) closed_seqs_memE
by (simp add: closed_seqs_memE constant_functionE)
lemma function_comp_is_closed_seq:
assumes "s ∈ closed_seqs R"
assumes "f ∈ carrier (Fun R)"
shows "f ∘ s ∈ closed_seqs R"
apply(rule closed_seqs_memI)
using assms(1) assms(2) closed_seqs_memE
by (metis comp_apply fun_add_eval_closed fun_add_zeroR function_zero_closed)
lemma function_sum_comp_is_seq_sum:
assumes "s ∈ closed_seqs R"
assumes "f ∈ carrier (Fun R)"
assumes "g ∈ carrier (Fun R)"
shows "(f ⊕⇘Fun R⇙ g) ∘ s = (f ∘ s) ⊕⇘R⇗ω⇖⇙ (g ∘ s)"
apply(rule ring_functions.function_ring_car_eqI[of R _ "UNIV :: nat set"])
apply (simp add: ring_functions_axioms)
using function_comp_is_closed_seq
apply (metis assms(1) assms(2) assms(3) fun_add_closed nat_seqs_def)
apply (metis assms(1) assms(2) assms(3) function_comp_is_closed_seq nat_seqs_def seq_plus_closed)
by (smt (verit) UNIV_eq_I assms(1) assms(2) assms(3) closed_seqs_memE comp_apply function_comp_is_closed_seq nat_seqs_def ring_functions.fun_add_eval_car ring_functions_axioms)
lemma function_mult_comp_is_seq_mult:
assumes "s ∈ closed_seqs R"
assumes "f ∈ carrier (Fun R)"
assumes "g ∈ carrier (Fun R)"
shows "(f ⊗⇘Fun R⇙ g) ∘ s = (f ∘ s) ⊗⇘R⇗ω⇖⇙ (g ∘ s)"
apply(rule ring_functions.function_ring_car_eqI[of R _ "UNIV :: nat set"])
apply (simp add: ring_functions_axioms)
using function_comp_is_closed_seq
apply (metis assms(1) assms(2) assms(3) fun_mult_closed nat_seqs_def)
apply (metis assms(1) assms(2) assms(3) function_comp_is_closed_seq nat_seqs_def seq_mult_closed)
by (metis (no_types, lifting) assms(1) assms(2) assms(3) comp_apply function_comp_is_closed_seq nat_seqs_def ring_functions.function_mult_eval_car ring_functions.function_ring_car_closed ring_functions_axioms)
lemma seq_plus_simp:
assumes "s ∈ closed_seqs R"
assumes "t ∈ closed_seqs R"
shows "(s ⊕⇘R⇗ω⇖⇙ t) k = s k ⊕ t k"
using assms unfolding nat_seqs_def
by (simp add: ring_functions.fun_add_eval_car ring_functions_axioms)
lemma seq_mult_simp:
assumes "s ∈ closed_seqs R"
assumes "t ∈ closed_seqs R"
shows "(s ⊗⇘R⇗ω⇖⇙ t) k = s k ⊗ t k"
using assms unfolding nat_seqs_def
by (simp add: ring_functions.function_mult_eval_car ring_functions_axioms)
lemma seq_one_simp:
"𝟭⇘R⇗ω⇖⇙ k = 𝟭"
by (simp add: nat_seqs_def ring_functions.function_one_eval ring_functions_axioms)
lemma seq_zero_simp:
"𝟬⇘R⇗ω⇖⇙ k = 𝟬"
by (simp add: nat_seqs_def ring_functions.function_zero_eval ring_functions_axioms)
lemma(in U_function_ring) ring_id_seq_comp:
assumes "s ∈ closed_seqs R"
shows "ring_id ∘ s = s"
apply(rule ring_functions.function_ring_car_eqI[of R _ "UNIV::nat set"])
using ring_functions_axioms apply auto[1]
apply (metis assms function_comp_is_closed_seq nat_seqs_def ring_id_closed)
apply (metis assms nat_seqs_def)
by (simp add: assms closed_seqs_memE ring_id_eval)
lemma(in U_function_ring) ring_seq_smult_closed:
assumes "s ∈ closed_seqs R"
assumes "a ∈ carrier R"
shows "a ⊙⇘R⇗ω⇖⇙ s ∈ closed_seqs R"
apply(rule closed_seqs_memI)
by (metis assms(1) assms(2) closed_seqs_memE nat_seqs_def ring_functions.function_smult_closed ring_functions_axioms)
lemma(in U_function_ring) ring_seq_smult_eval:
assumes "s ∈ closed_seqs R"
assumes "a ∈ carrier R"
shows "(a ⊙⇘R⇗ω⇖⇙ s) k = a ⊗ (s k)"
by (metis UNIV_I assms(1) assms(2) nat_seqs_def ring_functions.function_smult_eval ring_functions_axioms)
lemma(in U_function_ring) ring_seq_smult_comp_assoc:
assumes "s ∈ closed_seqs R"
assumes "f ∈ carrier (Fun R)"
assumes "a ∈ carrier R"
shows "((a ⊙⇘Fun R⇙ f) ∘ s) = a ⊙⇘R⇗ω⇖⇙ (f ∘ s)"
apply(rule ext)
using function_smult_eval[of a f] ring_seq_smult_eval[of "f ∘ s" a]
by (simp add: assms(1) assms(2) assms(3) closed_seqs_memE function_comp_is_closed_seq)
end
section‹Extensional Maps Between the Carriers of two Structures›
definition struct_maps :: "('a, 'c) partial_object_scheme ⇒ ('b, 'd) partial_object_scheme
⇒ ('a ⇒ 'b) set" where
"struct_maps T S = {f. (f ∈ (carrier T) → (carrier S)) ∧ f = restrict f (carrier T) }"
definition to_struct_map where
"to_struct_map T f = restrict f (carrier T)"
lemma to_struct_map_closed:
assumes "f ∈ (carrier T) → (carrier S)"
shows "to_struct_map T f ∈ (struct_maps T S)"
by (smt (verit) PiE_restrict Pi_iff assms mem_Collect_eq restrict_PiE struct_maps_def to_struct_map_def)
lemma struct_maps_memI:
assumes "⋀ x. x ∈ carrier T ⟹ f x ∈ carrier S"
assumes "⋀x. x ∉ carrier T ⟹ f x = undefined"
shows "f ∈ struct_maps T S"
proof-
have 0: " (f ∈ (carrier T) → (carrier S))"
using assms
by blast
have 1: "f = restrict f (carrier T)"
using assms
by (simp add: extensional_def extensional_restrict)
show ?thesis
using 0 1
unfolding struct_maps_def
by blast
qed
lemma struct_maps_memE:
assumes "f ∈ struct_maps T S"
shows "⋀ x. x ∈ carrier T ⟹ f x ∈ carrier S"
"⋀x. x ∉ carrier T ⟹ f x = undefined"
using assms unfolding struct_maps_def
apply blast
using assms unfolding struct_maps_def
by (metis (mono_tags, lifting) mem_Collect_eq restrict_apply)
text‹An abbreviation for restricted composition of function of functions. This is necessary for the composition of two struct maps to again be a struct map.›
abbreviation(input) rcomp
where "rcomp ≡ FuncSet.compose"
lemma struct_map_comp:
assumes "g ∈ (struct_maps T S)"
assumes "f ∈ (struct_maps S U)"
shows "rcomp (carrier T) f g ∈ (struct_maps T U)"
proof(rule struct_maps_memI)
show "⋀x. x ∈ carrier T ⟹ rcomp (carrier T) f g x ∈ carrier U"
using assms struct_maps_memE(1)
by (metis compose_eq)
show " ⋀x. x ∉ carrier T ⟹ rcomp (carrier T) f g x = undefined"
by (meson compose_extensional extensional_arb)
qed
lemma r_comp_is_compose:
assumes "g ∈ (struct_maps T S)"
assumes "f ∈ (struct_maps S U)"
assumes "a ∈ (carrier T)"
shows "(rcomp (carrier T) f g) a = (f ∘ g) a"
by (simp add: FuncSet.compose_def assms(3))
lemma r_comp_not_in_car:
assumes "g ∈ (struct_maps T S)"
assumes "f ∈ (struct_maps S U)"
assumes "a ∉ (carrier T)"
shows "(rcomp (carrier T) f g) a = undefined"
by (simp add: FuncSet.compose_def assms(3))
text‹The reverse composition of two struct maps:›
definition pullback ::
"('a, 'd) partial_object_scheme ⇒ ('a ⇒ 'b) ⇒ ('b ⇒ 'c) ⇒ ('a ⇒ 'c)" where
"pullback T f g = rcomp (carrier T) g f"
lemma pullback_closed:
assumes "f ∈ (struct_maps T S)"
assumes "g ∈ (struct_maps S U)"
shows "pullback T f g ∈ (struct_maps T U)"
by (metis assms(1) assms(2) pullback_def struct_map_comp)
text‹Composition of struct maps which takes the structure itself rather than the carrier as a parameter:›
definition pushforward ::
"('a, 'd) partial_object_scheme ⇒ ('b ⇒ 'c) ⇒ ('a ⇒ 'b) ⇒ ('a ⇒ 'c)" where
"pushforward T f g ≡ rcomp (carrier T) f g"
lemma pushforward_closed:
assumes "g ∈ (struct_maps T S)"
assumes "f ∈ (struct_maps S U)"
shows "pushforward T f g ∈ (struct_maps T U)"
using assms(1) assms(2) struct_map_comp
by (metis pushforward_def)
end