Theory utp_sequent

section ‹ Sequent Calculus ›

theory utp_sequent
  imports utp_pred_laws
begin

definition sequent :: "'α upred ⇒ 'α upred ⇒ bool" (infixr "⊩" 15) where
[upred_defs]: "sequent P Q = (Q ⊑ P)"

abbreviation sequent_triv ("⊩ _" [15] 15) where "⊩ P ≡ (true ⊩ P)"

translations
  "⊩ P" <= "true ⊩ P"

lemma sTrue: "P ⊩ true"
  by pred_auto

lemma sAx: "P ⊩ P"
  by pred_auto

lemma sNotI: "Γ ∧ P ⊩ false ⟹ Γ ⊩ ¬ P"
  by pred_auto

lemma sConjI: "⟦ Γ ⊩ P; Γ ⊩ Q ⟧ ⟹ Γ ⊩ P ∧ Q"
  by pred_auto

lemma sImplI: "⟦ (Γ ∧ P) ⊩ Q ⟧ ⟹ Γ ⊩ (P ⇒ Q)"
  by pred_auto

end