Theory Phi_BI.Arrow_st

theory Arrow_st
  imports Algebras
begin


datatype 'a arrow_st = Arrow_st (s: 'a) (t: 'a) (infix "➤" 60)

lemma split_arrow_All:
  ‹ All P ⟷ (∀a b. P (a ➤ b)) ›
  by (metis arrow_st.collapse)

lemma split_arrow_Ex:
  ‹ Ex P ⟷ (∃a b. P (a ➤ b)) ›
  by (metis arrow_st.collapse)

lemma split_arrow_all:
  ‹ Pure.all P ≡ (⋀a b. PROP P (a ➤ b)) ›
proof
  fix a b :: 'a
  assume ‹⋀x. PROP P x›
  then show ‹PROP P (a ➤ b)› .
next
  fix x :: ‹'a arrow_st›
  assume ‹⋀a b. PROP P (a ➤ b)›
  from ‹PROP P (s x ➤ t x)› show ‹PROP P x› by simp
qed

instantiation arrow_st :: (type) partial_add_cancel begin

definition plus_arrow_st :: ‹'a arrow_st ⇒ 'a arrow_st ⇒ 'a arrow_st›
  where ‹plus_arrow_st a b = (s a ➤ t b)›

definition dom_of_add_arrow_st :: ‹'a arrow_st ⇒ 'a arrow_st ⇒ bool›
  where ‹dom_of_add_arrow_st a b ⟷ t a = s b›

lemma plus_arrow[iff]:
  ‹ (ss ➤ tt) + (tt ➤ uu) = (ss ➤ uu) ›
  unfolding plus_arrow_st_def
  by simp

lemma dom_of_add_arrow_st[iff]:
  ‹ a ##⇩+ b ⟷ t a = s b ›
  unfolding dom_of_add_arrow_st_def
  by simp

instance by (standard, clarsimp simp: split_arrow_all)

end

lemma plus_arrow_st_s[iff]:
  ‹ s (a + b) = s a ›
  unfolding plus_arrow_st_def
  by simp

lemma plus_arrow_st_t[iff]:
  ‹ t (a + b) = t b ›
  unfolding plus_arrow_st_def
  by simp

instance arrow_st :: (type) partial_cancel_semigroup_add
  by (standard; clarsimp simp add: split_arrow_all)



hide_const (open) s t

end