Theory Lang

(*  Title:       A while language
    Author:      Tobias Nipkow, 2001/2006
    Maintainer:  Tobias Nipkow
*)

section "Hoare Logics for While"

theory Lang imports Main begin

subsection‹The language \label{sec:lang}›

text‹We start by declaring a type of states:›

typedecl state

text‹\noindent
Our approach is completely parametric in the state space.
We define expressions (‹bexp›) as functions from states
to the booleans:›

type_synonym bexp = "state ⇒ bool"

text‹
Instead of modelling the syntax of boolean expressions, we
model their semantics. The (abstract and concrete)
syntax of our programming is defined as a recursive datatype:
›

datatype com = Do "(state ⇒ state set)"
             | Semi  com com            ("_; _"  [60, 60] 10)
             | Cond  bexp com com     ("IF _ THEN _ ELSE _"  60)
             | While bexp com           ("WHILE _ DO _"  60)
             | Local "(state ⇒ state)" com "(state ⇒ state ⇒ state)"
               ("LOCAL _; _; _" [0,0,60] 60)

text‹\noindent Statements in this language are called
\emph{commands}.  They are modelled as terms of type @{typ
com}. @{term"Do f"} represents an atomic nondeterministic command that
changes the state from @{term s} to some element of @{term"f s"}.
Thus the command that does nothing, often called \texttt{skip}, can be
represented by @{term"Do(λs. {s})"}. Again we have chosen to model the
semantics rather than the syntax, which simplifies matters
enormously. Of course it means that we can no longer talk about
certain syntactic matters, but that is just fine.

The constructors @{term Semi}, @{term Cond} and @{term While}
represent sequential composition, conditional and while-loop.
The annotations allow us to write
\begin{center}
@{term"c⇩1;c⇩2"} \qquad @{term"IF b THEN c⇩1 ELSE c⇩2"}
 \qquad @{term"WHILE b DO c"}
\end{center}
instead of @{term[source]"Semi c⇩1 c⇩2"}, @{term[source]"Cond b c⇩1 c⇩2"}
and @{term[source]"While b c"}.

The command @{term"LOCAL f;c;g"} applies function ‹f› to the state,
executes @{term c}, and then combines initial and final state via function
‹g›. More below.
The semantics of commands is defined inductively by a so-called
big-step semantics.›

inductive
  exec :: "state ⇒ com ⇒ state ⇒ bool" ("_/ -_→/ _" [50,0,50] 50)
where
  (*<*)Do:(*>*)"t ∈ f s ⟹ s -Do f→ t"

| (*<*)Semi:(*>*)"⟦ s0 -c1→ s1; s1 -c2→ s2 ⟧ ⟹ s0 -c1;c2→ s2"

| (*<*)IfT:(*>*)"⟦  b s; s -c1→ t ⟧ ⟹ s -IF b THEN c1 ELSE c2→ t"
| (*<*)IfF:(*>*)"⟦ ¬b s; s -c2→ t ⟧ ⟹ s -IF b THEN c1 ELSE c2→ t"

| (*<*)WhileF:(*>*)"¬b s ⟹ s -WHILE b DO c→ s"
| (*<*)WhileT:(*>*)"⟦ b s; s -c→ t; t -WHILE b DO c→ u ⟧ ⟹ s -WHILE b DO c→ u"

| (*<*)Local:(*>*) "f s -c→ t ⟹ s -LOCAL f; c; g→ g s t"

text‹Assuming that the state is a function from variables to values,
the declaration of a new local variable ‹x› with inital value
‹a› can be modelled as
‹LOCAL (λs. s(x := a s)); c; (λs t. t(x := s x))›.›

lemma exec_Do_iff[iff]: "(s -Do f→ t) = (t ∈ f s)"
by(auto elim: exec.cases intro:exec.intros)

lemma [iff]: "(s -c;d→ u) = (∃t. s -c→ t ∧ t -d→ u)"
by(best elim: exec.cases intro:exec.intros)

lemma [iff]: "(s -IF b THEN c ELSE d→ t) =
              (s -if b s then c else d→ t)"
apply auto
apply(blast elim: exec.cases intro:exec.intros)+
done

lemma [iff]: "(s -LOCAL f; c; g→ u) = (∃t. f s -c→ t ∧ u = g s t)"
by(fastforce elim: exec.cases intro:exec.intros)

lemma unfold_while:
 "(s -WHILE b DO c→ u) =
  (s -IF b THEN c;WHILE b DO c ELSE Do(λs. {s})→ u)"
by(auto elim: exec.cases intro:exec.intros split:if_split_asm)


lemma while_lemma[rule_format]:
"s -w→ t ⟹ ∀b c. w = WHILE b DO c ∧ P s ∧
                    (∀s s'. P s ∧ b s ∧ s -c→ s' ⟶ P s') ⟶ P t ∧ ¬b t"
apply(erule exec.induct)
apply clarify+
defer
apply clarify+
apply(subgoal_tac "P t")
apply blast
apply blast
done

lemma while_rule:
 "⟦s -WHILE b DO c→ t; P s; ∀s s'. P s ∧ b s ∧ s -c→ s' ⟶ P s'⟧
  ⟹ P t ∧ ¬b t"
apply(drule while_lemma)
prefer 2 apply assumption
apply blast
done

end