Theory W0

(*
   Authors: Asta Halkjær From & Jørgen Villadsen, DTU Compute
*)

chapter ‹The W0 Theory›

theory W0 imports System_W begin

notation (input) Imp (infixr ‹❙⟶› 25)

notation (input) Neg (‹❙¬ _› [40] 40)

abbreviation (input) Dis (infixr ‹❙∨› 30) where ‹p ❙∨ q ≡ ❙¬ p ❙⟶ q›

abbreviation (input) Con (infixr ‹❙∧› 35) where ‹p ❙∧ q ≡ ❙¬ (p ❙⟶ ❙¬ q)›

proposition
  ‹¬ (I ⊨ ⊥)›
  ‹(I ⊨ p ❙⟶ q) = ((I ⊨ p) ⟶ (I ⊨ q))›
  ‹(I ⊨ ❙¬ p) = (¬ (I ⊨ p))›
  ‹(I ⊨ p ❙∨ q) = ((I ⊨ p) ∨ (I ⊨ q))›
  ‹(I ⊨ p ❙∧ q) = ((I ⊨ p) ∧ (I ⊨ q))›
  by simp_all

end