Theory ETTS_Tests

(* Title: ETTS/Tests/ETTS_Tests.thy
   Author: Mihails Milehins
   Copyright 2021 (C) Mihails Milehins

A test suite for the ETTS.
*)

section‹A test suite for ETTS›
theory ETTS_Tests
  imports
    "../ETTS_Auxiliary"
    Conditional_Transfer_Rule.IML_UT
begin



subsectionamend_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 ow 50) 
    and ls :: "['bo, 'bo]  bool" (infix <ow 50)
    and f :: "['ao, 'bo]  'co"
  assumes closed_f: " a  UA; b  UB   f a b  UC"
begin

notation le ('(≤ow'))
  and le (infix ow 50) 
  and ls ('(<ow')) 
  and ls (infix <ow 50)

tts_register_sbts (≤ow) | 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 (<ow) | 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
MLLecker.test_group @{context} () [etts_test_amend_ctxt_data.test_suite]
end



subsectiontts_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". 
›

(*the following theorem is restated for forward compatibility*)
lemma exI': "P x  x. P x" by auto

class tta_mult =
  fixes tta_mult :: "'a  'a  'a" (infixl "*tta" 65)

class tta_semigroup = tta_mult +
  assumes tta_assoc[simp]: "(a *tta b) *tta c = a *tta (b *tta c)"

definition set_mult :: "'a::tta_mult set  'a set  'a set" (infixl "*tta" 65) 
  where "set_mult S T = {s *tta t | s t. s  S  t  T}"

definition left_ideal :: "'a::tta_mult set  bool"
  where "left_ideal T  (s. tT. s *tta t  T)"

lemma left_idealI[intro]:
  assumes "s t. t  T  s *tta 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 *tta t  T"
  using assms unfolding left_ideal_def by simp

lemma left_ideal_set_mult_iff: "left_ideal T  UNIV *tta 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 *tta b) = f a *tta 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 *tta t  T" for s t by auto
  with t show "fs *tta 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 *ow.a 70) and times_b (infixl *ow.b 70) +
  fixes f :: "'a  'b"
  assumes f_hom: "f (a *ow.a b) = f a *ow.b f b"

lemma semigroup_mult_hom_with[ud_with]:
  "tta_semigroup_hom = semigroup_mult_hom_with (*tta) (*tta)"
  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 *ow 70)
  assumes f_closed: " a  U; b  U   a *ow b  U"
    and assoc: " a  U; b  U; c  U   a *ow b *ow c = a *ow (b *ow c)"
begin

notation f (infixl *ow 70)

lemma f_closed'[simp]: "xU. yU. x *ow y  U" by (simp add: f_closed)

tts_register_sbts (*ow) | U by (rule tts_AA_A_transfer[OF f_closed])

end

locale times_ow =
  fixes U :: "'ag set" and times :: "['ag, 'ag]  'ag" (infixl *ow 70)
  assumes times_closed[simp, intro]: " a  U; b  U   a *ow b  U"
begin

notation times (infixl *ow 70)

lemma times_closed'[simp]: "xU. yU. x *ow y  U" by simp

tts_register_sbts (*ow) | 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 *ow b *ow c = a *ow (b *ow c)"
begin

sublocale mult: semigroup_ow U (*ow) 
  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 *ow.a 70) 
    and times_b (infixl *ow.b 70) +
  fixes f :: "'a  'b"
  assumes f_closed[simp]: "a  UA  f a  UB"
    and f_hom: " a  UA; b  UA   f (a *ow.a b) = f a *ow.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 (*ow.a) T"
    and "f ` UA = UB"
  shows "left_ideal_ow UB (*ow.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 *ow.a t  T" for s t 
    unfolding left_ideal_ow_def by simp
  with assms(1) s t fs show "fs *ow.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 (*tta) (*tta)"
  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: ((*tta)::[?'a::tta_semigroup, ?'a]  ?'a to (*ow.a))
    and ((*tta)::[?'b::tta_semigroup, ?'b]  ?'b to (*ow.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
MLLecker.test_group @{context} () [etts_test_tts_algorithm.test_suite]
end

end



subsectiontts_register_sbts›

context
  fixes f :: "'a  'b  'c"
    and UA :: "'a set"
begin
ML_file‹ETTS_TEST_TTS_REGISTER_SBTS.ML›
MLLecker.test_group @{context} () [etts_test_tts_register_sbts.test_suite]
end

end