Theory ETTS_Tests
section‹A test suite for ETTS›
theory ETTS_Tests
imports
"../ETTS_Auxiliary"
Conditional_Transfer_Rule.IML_UT
begin
subsection‹‹amend_ctxt_data››
ML_file‹ETTS_TEST_AMEND_CTXT_DATA.ML›
locale test_amend_ctxt_data =
fixes UA :: "'ao set" and UB :: "'bo set" and UC :: "'co set"
and le :: "['ao, 'ao] ⇒ bool" (infix ‹≤⇩o⇩w› 50)
and ls :: "['bo, 'bo] ⇒ bool" (infix ‹<⇩o⇩w› 50)
and f :: "['ao, 'bo] ⇒ 'co"
assumes closed_f: "⟦ a ∈ UA; b ∈ UB ⟧ ⟹ f a b ∈ UC"
begin
notation le (‹'(≤⇩o⇩w')›)
and le (infix ‹≤⇩o⇩w› 50)
and ls (‹'(<⇩o⇩w')›)
and ls (infix ‹<⇩o⇩w› 50)
tts_register_sbts ‹(≤⇩o⇩w)› | UA
proof-
assume "Domainp AOA = (λx. x ∈ UA)" "bi_unique AOA" "right_total AOA"
from tts_AA_eq_transfer[OF this] show ?thesis by auto
qed
tts_register_sbts ‹(<⇩o⇩w)› | UB
proof-
assume "Domainp BOA = (λx. x ∈ UB)" "bi_unique BOA" "right_total BOA"
from tts_AA_eq_transfer[OF this] show ?thesis by auto
qed
tts_register_sbts f | UA and UB and UC
proof-
assume
"Domainp AOC = (λx. x ∈ UA)" "bi_unique AOC" "right_total AOC"
"Domainp BOB = (λx. x ∈ UB)" "bi_unique BOB" "right_total BOB"
"Domainp COA = (λx. x ∈ UC)" "bi_unique COA" "right_total COA"
from tts_AB_C_transfer[OF closed_f this] show ?thesis by auto
qed
end
context test_amend_ctxt_data
begin
ML‹
Lecker.test_group @{context} () [etts_test_amend_ctxt_data.test_suite]
›
end
subsection‹‹tts_algorithm››
text‹
Some of the elements of the content of this section are based on the
elements of the content of \<^cite>‹"cain_nine_2019"›.
›
lemma exI': "P x ⟹ ∃x. P x" by auto
class tta_mult =
fixes tta_mult :: "'a ⇒ 'a ⇒ 'a" (infixl "*⇩t⇩t⇩a" 65)
class tta_semigroup = tta_mult +
assumes tta_assoc[simp]: "(a *⇩t⇩t⇩a b) *⇩t⇩t⇩a c = a *⇩t⇩t⇩a (b *⇩t⇩t⇩a c)"
definition set_mult :: "'a::tta_mult set ⇒ 'a set ⇒ 'a set" (infixl "❙*⇩t⇩t⇩a" 65)
where "set_mult S T = {s *⇩t⇩t⇩a t | s t. s ∈ S ∧ t ∈ T}"
definition left_ideal :: "'a::tta_mult set ⇒ bool"
where "left_ideal T ⟷ (∀s. ∀t∈T. s *⇩t⇩t⇩a t ∈ T)"
lemma left_idealI[intro]:
assumes "⋀s t. t ∈ T ⟹ s *⇩t⇩t⇩a t ∈ T"
shows "left_ideal T"
using assms unfolding left_ideal_def by simp
lemma left_idealE[elim]:
assumes "left_ideal T"
obtains "⋀s t. t ∈ T ⟹ s *⇩t⇩t⇩a t ∈ T"
using assms unfolding left_ideal_def by simp
lemma left_ideal_set_mult_iff: "left_ideal T ⟷ UNIV ❙*⇩t⇩t⇩a T ⊆ T"
unfolding left_ideal_def set_mult_def by auto
ud ‹set_mult›
ud ‹left_ideal›
ctr relativization
synthesis ctr_simps
assumes [transfer_domain_rule]: "Domainp A = (λx. x ∈ U)"
and [transfer_rule]: "bi_unique A" "right_total A"
trp (?'a A)
in set_mult_ow: set_mult.with_def
and left_ideal_ow: left_ideal.with_def
locale tta_semigroup_hom =
fixes f :: "'a::tta_semigroup ⇒ 'b::tta_semigroup"
assumes hom: "f (a *⇩t⇩t⇩a b) = f a *⇩t⇩t⇩a f b"
context tta_semigroup_hom
begin
lemma tta_left_ideal_closed:
assumes "left_ideal T" and "surj f"
shows "left_ideal (f ` T)"
unfolding left_ideal_def
proof(intro allI ballI)
fix fs ft assume prems: "ft ∈ f ` T"
then obtain t where t: "t ∈ T" and ft_def: "ft = f t" by clarsimp
from assms(2) obtain s where fs_def: "fs = f s" by auto
from assms have "t ∈ T ⟹ s *⇩t⇩t⇩a t ∈ T" for s t by auto
with t show "fs *⇩t⇩t⇩a ft ∈ f ` T"
unfolding ft_def fs_def hom[symmetric] by simp
qed
end
locale semigroup_mult_hom_with =
dom: tta_semigroup times_a + cod: tta_semigroup times_b
for times_a (infixl ‹*⇩o⇩w⇩.⇩a› 70) and times_b (infixl ‹*⇩o⇩w⇩.⇩b› 70) +
fixes f :: "'a ⇒ 'b"
assumes f_hom: "f (a *⇩o⇩w⇩.⇩a b) = f a *⇩o⇩w⇩.⇩b f b"
lemma semigroup_mult_hom_with[ud_with]:
"tta_semigroup_hom = semigroup_mult_hom_with (*⇩t⇩t⇩a) (*⇩t⇩t⇩a)"
unfolding
semigroup_mult_hom_with_def tta_semigroup_hom_def
class.tta_semigroup_def semigroup_mult_hom_with_axioms_def
by auto
locale semigroup_ow =
fixes U :: "'ag set" and f :: "['ag, 'ag] ⇒ 'ag" (infixl ‹❙*⇩o⇩w› 70)
assumes f_closed: "⟦ a ∈ U; b ∈ U ⟧ ⟹ a ❙*⇩o⇩w b ∈ U"
and assoc: "⟦ a ∈ U; b ∈ U; c ∈ U ⟧ ⟹ a ❙*⇩o⇩w b ❙*⇩o⇩w c = a ❙*⇩o⇩w (b ❙*⇩o⇩w c)"
begin
notation f (infixl ‹❙*⇩o⇩w› 70)
lemma f_closed'[simp]: "∀x∈U. ∀y∈U. x ❙*⇩o⇩w y ∈ U" by (simp add: f_closed)
tts_register_sbts ‹(❙*⇩o⇩w)› | U by (rule tts_AA_A_transfer[OF f_closed])
end
locale times_ow =
fixes U :: "'ag set" and times :: "['ag, 'ag] ⇒ 'ag" (infixl ‹*⇩o⇩w› 70)
assumes times_closed[simp, intro]: "⟦ a ∈ U; b ∈ U ⟧ ⟹ a *⇩o⇩w b ∈ U"
begin
notation times (infixl ‹*⇩o⇩w› 70)
lemma times_closed'[simp]: "∀x∈U. ∀y∈U. x *⇩o⇩w y ∈ U" by simp
tts_register_sbts ‹(*⇩o⇩w)› | U by (rule tts_AA_A_transfer[OF times_closed])
end
locale semigroup_mult_ow = times_ow U times
for U :: "'ag set" and times +
assumes mult_assoc:
"⟦ a ∈ U; b ∈ U; c ∈ U ⟧ ⟹ a *⇩o⇩w b *⇩o⇩w c = a *⇩o⇩w (b *⇩o⇩w c)"
begin
sublocale mult: semigroup_ow U ‹(*⇩o⇩w)›
by unfold_locales (auto simp: times_closed' mult_assoc)
end
locale semigroup_mult_hom_ow =
dom: semigroup_mult_ow UA times_a +
cod: semigroup_mult_ow UB times_b
for UA :: "'a set"
and UB :: "'b set"
and times_a (infixl ‹*⇩o⇩w⇩.⇩a› 70)
and times_b (infixl ‹*⇩o⇩w⇩.⇩b› 70) +
fixes f :: "'a ⇒ 'b"
assumes f_closed[simp]: "a ∈ UA ⟹ f a ∈ UB"
and f_hom: "⟦ a ∈ UA; b ∈ UA ⟧ ⟹ f (a *⇩o⇩w⇩.⇩a b) = f a *⇩o⇩w⇩.⇩b f b"
begin
lemma f_closed'[simp]: "f ` UA ⊆ UB" by auto
tts_register_sbts f | UA and UB by (rule tts_AB_transfer[OF f_closed'])
end
context semigroup_mult_hom_ow
begin
lemma tta_left_ideal_ow_closed:
assumes "T ⊆ UA"
and "left_ideal_ow UA (*⇩o⇩w⇩.⇩a) T"
and "f ` UA = UB"
shows "left_ideal_ow UB (*⇩o⇩w⇩.⇩b) (f ` T)"
unfolding left_ideal_ow_def
proof(intro ballI)
fix fs ft assume ft: "ft ∈ f ` T" and fs: "fs ∈ UB"
then obtain t where t: "t ∈ T" and ft_def: "ft = f t" by auto
from assms(3) fs obtain s where fs_def: "fs = f s" and s: "s ∈ UA" by auto
from assms have "⟦ s ∈ UA; t ∈ T ⟧ ⟹ s *⇩o⇩w⇩.⇩a t ∈ T" for s t
unfolding left_ideal_ow_def by simp
with assms(1) s t fs show "fs *⇩o⇩w⇩.⇩b ft ∈ f ` T"
using f_hom[symmetric, OF s] unfolding ft_def fs_def by auto
qed
end
lemma semigroup_mult_ow: "class.tta_semigroup = semigroup_mult_ow UNIV"
unfolding
class.tta_semigroup_def semigroup_mult_ow_def
semigroup_mult_ow_axioms_def times_ow_def
by simp
lemma semigroup_mult_hom_ow:
"tta_semigroup_hom = semigroup_mult_hom_ow UNIV UNIV (*⇩t⇩t⇩a) (*⇩t⇩t⇩a)"
unfolding
tta_semigroup_hom_def semigroup_mult_hom_ow_axioms_def
semigroup_mult_hom_ow_def semigroup_mult_ow_def
semigroup_mult_ow_axioms_def times_ow_def
by simp
context
includes lifting_syntax
begin
lemma semigroup_transfer[transfer_rule]:
assumes [transfer_rule]: "bi_unique A" "right_total A"
shows
"((A ===> A ===> A) ===> (=))
(semigroup_ow (Collect (Domainp A))) semigroup"
proof-
let ?P = "((A ===> A ===> A) ===> (=))"
let ?semigroup_ow = "semigroup_ow (Collect (Domainp A))"
let ?rf_UNIV =
"(λf::['b, 'b] ⇒ 'b. (∀x y. x ∈ UNIV ⟶ y ∈ UNIV ⟶ f x y ∈ UNIV))"
have "?P ?semigroup_ow (λf. ?rf_UNIV f ∧ semigroup f)"
unfolding semigroup_ow_def semigroup_def
apply transfer_prover_start
apply transfer_step+
by simp
thus ?thesis by simp
qed
lemma semigroup_mult_transfer[transfer_rule]:
assumes [transfer_rule]: "bi_unique A" "right_total A"
shows
"((A ===> A ===> A) ===> (=))
(semigroup_mult_ow (Collect (Domainp A)))
class.tta_semigroup"
proof -
let ?P = ‹((A ===> A ===> A) ===> (=))›
and ?semigroup_mult_ow =
‹(λf. semigroup_mult_ow (Collect (Domainp A)) f)›
and ?rf_UNIV =
‹(λf::['b, 'b] ⇒ 'b. (∀x y. x ∈ UNIV ⟶ y ∈ UNIV ⟶ f x y ∈ UNIV))›
have "?P ?semigroup_mult_ow (λf. ?rf_UNIV f ∧ class.tta_semigroup f)"
unfolding
semigroup_mult_ow_def class.tta_semigroup_def
semigroup_mult_ow_axioms_def times_ow_def
apply transfer_prover_start
apply transfer_step+
by simp
thus ?thesis by simp
qed
lemma semigroup_mult_hom_transfer[transfer_rule]:
assumes [transfer_rule]:
"bi_unique A" "right_total A" "bi_unique B" "right_total B"
shows
"((A ===> A ===> A) ===> (B ===> B ===> B) ===> (A ===> B) ===> (=))
(semigroup_mult_hom_ow (Collect (Domainp A)) (Collect (Domainp B)))
semigroup_mult_hom_with"
proof-
let ?PA = "A ===> A ===> A"
and ?PB = "B ===> B ===> B"
and ?semigroup_mult_hom_ow =
‹
λtimes_a times_b f. semigroup_mult_hom_ow
(Collect (Domainp A)) (Collect (Domainp B)) times_a times_b f
›
let ?closed = ‹λf::'b⇒'d . ∀a. a ∈ UNIV ⟶ f a ∈ UNIV›
have
"(?PA ===> ?PB ===> (A ===> B) ===> (=))
?semigroup_mult_hom_ow
(
λtimes_a times_b f.
?closed f ∧ semigroup_mult_hom_with times_a times_b f
)"
unfolding
times_ow_def
semigroup_mult_hom_ow_def
semigroup_mult_hom_ow_axioms_def
semigroup_mult_hom_with_def
semigroup_mult_hom_with_axioms_def
apply transfer_prover_start
apply transfer_step+
by blast
thus ?thesis by simp
qed
end
context semigroup_mult_hom_ow
begin
ML_file‹ETTS_TEST_TTS_ALGORITHM.ML›
named_theorems semigroup_mult_hom_ow_test_simps
lemmas [semigroup_mult_hom_ow_test_simps] =
ctr_simps_Collect_mem_eq
ctr_simps_in_iff
tts_context
tts: (?'a to UA) and (?'b to UB)
sbterms: (‹(*⇩t⇩t⇩a)::[?'a::tta_semigroup, ?'a] ⇒ ?'a› to ‹(*⇩o⇩w⇩.⇩a)›)
and (‹(*⇩t⇩t⇩a)::[?'b::tta_semigroup, ?'b] ⇒ ?'b› to ‹(*⇩o⇩w⇩.⇩b)›)
and (‹?f::?'a::tta_semigroup ⇒ ?'b::tta_semigroup› to f)
rewriting semigroup_mult_hom_ow_test_simps
substituting semigroup_mult_hom_ow_axioms
and dom.semigroup_mult_ow_axioms
and cod.semigroup_mult_ow_axioms
eliminating ‹UA ≠ {}› and ‹UB ≠ {}›
through (auto simp only: left_ideal_ow_def)
begin
ML‹
Lecker.test_group @{context} () [etts_test_tts_algorithm.test_suite]
›
end
end
subsection‹‹tts_register_sbts››
context
fixes f :: "'a ⇒ 'b ⇒ 'c"
and UA :: "'a set"
begin
ML_file‹ETTS_TEST_TTS_REGISTER_SBTS.ML›
ML‹
Lecker.test_group @{context} () [etts_test_tts_register_sbts.test_suite]
›
end
end