Theory Lang

Up to index of Isabelle/HOL/Abstract-Hoare-Logics

theory Lang
imports Main
(*  Title:       A while language    Author:      Tobias Nipkow, 2001/2006    Maintainer:  Tobias Nipkow*)header "Hoare Logics for While"theory Lang imports Main beginsubsection{* The language \label{sec:lang} *}text{* We start by declaring a type of states: *}typedecl statetext{*\noindentOur approach is completely parametric in the state space.We define expressions (@{text bexp}) as functions from statesto the booleans: *}type_synonym bexp = "state => bool"text{*Instead of modelling the syntax of boolean expressions, wemodel 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 @{typcom}. @{term"Do f"} represents an atomic nondeterministic command thatchanges the state from @{term s} to some element of @{term"f s"}.Thus the command that does nothing, often called \texttt{skip}, can berepresented by @{term"Do(λs. {s})"}. Again we have chosen to model thesemantics rather than the syntax, which simplifies mattersenormously. Of course it means that we can no longer talk aboutcertain 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 @{text f} to the state,executes @{term c}, and then combines initial and final state via function@{text g}. More below.The semantics of commands is defined inductively by a so-calledbig-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 @{text x} with inital value@{text a} can be modelled as@{text"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 autoapply(blast elim: exec.cases intro:exec.intros)+donelemma [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:split_if_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+deferapply clarify+apply(subgoal_tac "P t")apply blastapply blastdonelemma 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 assumptionapply blastdoneend