# Theory Hoare

section ‹Inductive definition of Hoare logic for partial correctness›
theory Hoare
imports Natural
begin
text ‹
Completeness is taken relative to completeness of the underlying logic.
Two versions of completeness proof: nested single recursion
vs. simultaneous recursion in call rule
›
type_synonym 'a assn = "'a => state => bool"
translations
(type) "'a assn" <= (type) "'a => state => bool"
definition
state_not_singleton :: bool where
"state_not_singleton = (∃s t::state. s ~= t)"
definition
peek_and :: "'a assn => (state => bool) => 'a assn" (infixr "&>" 35) where
"peek_and P p = (%Z s. P Z s & p s)"