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

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"

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
@{term"c1;c2"} \qquad @{term"IF b THEN c1 ELSE c2"}
 \qquad @{term"WHILE b DO c"}
instead of @{term[source]"Semi c1 c2"}, @{term[source]"Cond b c1 c2"}
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.›

  exec :: "state  com  state  bool" ("_/ -_/ _" [50,0,50] 50)
  (*<*)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)+

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+
apply clarify+
apply(subgoal_tac "P t")
apply blast
apply blast

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