| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/UTP/utp/ Datei vom 29.4.2026 mit Größe 989 B |
|
Quelle utp_sequent.thySprache: Isabelle |
|||||||||||||||
|
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
¤ Dauer der Verarbeitung: 0.7 Sekunden (vorverarbeitet am 2026-06-12) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-06-12