Theory IMP

(*File: IMP.thy*)
(*Authors: Lennart Beringer and Martin Hofmann, LMU Munich 2008*)
theory IMP imports Main begin
section ‹The language IMP›

text‹\label{sec:IMP}In this section we define a simple imperative programming
language. Syntax and operational semantics are as in \<^cite>‹"Winskel93"›,
except that we enrich the language with a single unnamed,
parameterless procedure. Both, this section and the following one
merely set the basis for the development described in the later
sections and largely follow the approach to formalize program logics
advocated by Kleymann, Nipkow, and others - see for example
\<^cite>‹"KleymannPhD" and "Nipkow-CSL02" and "Nipkow-AFP-AHL"›.›

subsection‹Syntax› 

text‹We start from unspecified categories of program variables and
values.›

typedecl Var
typedecl Val

text‹Arithmetic expressions are inductively built up from variables,
values, and binary operators which are modeled as meta-logical
functions over values. Similarly, boolean expressions are built up
from arithmetic expressions using binary boolean operators which are 
modeled as functions of the ambient logic HOL.›

datatype Expr =
   varE Var
 | valE Val
 | opE "Val ⇒ Val ⇒ Val" Expr Expr

datatype BExpr = compB "Val ⇒ Val ⇒ bool" Expr Expr

text‹Commands are the usual ones for an imperative language, plus the
command $\mathit{Call}$ which stands for the invocation of a single
(unnamed, parameterless) procedure.›

datatype IMP =
    Skip 
  | Assign Var Expr
  | Comp IMP IMP
  | While BExpr IMP
  | Iff BExpr IMP IMP
  | Call

text‹The body of this procedure is identified by the following
constant.›

consts body :: IMP

subsection‹Dynamic semantics›

text‹States are given by stores - in our case, HOL functions
mapping program variables to values.›

type_synonym State = "Var ⇒ Val"

definition update :: "State ⇒ Var ⇒ Val ⇒ State"
where "update s x v = (λ y . if x=y then v else s y)"

text‹The evaluation of expressions is defined inductively, as
standard.›

primrec evalE::"Expr ⇒ State ⇒ Val"
where
"evalE (varE x) s = s x" |
"evalE (valE v) s = v" |
"evalE (opE f e1 e2) s = f (evalE e1 s) (evalE e2 s)"

primrec evalB::"BExpr ⇒ State ⇒ bool"
where
"evalB (compB f e1 e2) s = f (evalE e1 s) (evalE e2 s)"

text‹The operational semantics is a standard big-step relation, with
a height index that facilitates the Kleymann-Nipkow-style~\<^cite>‹"KleymannPhD" and "Nipkow-CSL02"›
soundness proof of the program logic.›

inductive_set Semn :: "(State × IMP × nat × State) set" where
 SemSkip: "(s,Skip,1,s) : Semn" 

| SemAssign:
  "⟦ t = update s x (evalE e s)⟧ ⟹ (s,Assign x e,1,t):Semn"

| SemComp:
  "⟦ (s,c1,n,r):Semn; (r,c2,m,t):Semn; k=(max n m)+1⟧
   ⟹ (s,Comp c1 c2,k,t):Semn"

| SemWhileT:
  "⟦evalB b s; (s,c,n,r):Semn; (r,While b c,m,t):Semn; 
       k=((max n m)+1)⟧
   ⟹ (s,While b c,k,t):Semn"

| SemWhileF: "⟦¬ (evalB b s); t=s⟧ ⟹ (s,While b c,1,t):Semn"

| SemTrue:
  "⟦evalB b s; (s,c1,n,t):Semn ⟧ ⟹ (s,Iff b c1 c2,n+1,t):Semn"

| SemFalse:
  "⟦¬ (evalB b s); (s,c2,n,t):Semn⟧ ⟹ (s,Iff b c1 c2,n+1,t):Semn"

| SemCall: "(s,body,n,t):Semn ⟹ (s,Call,n+1,t):Semn"
(*
 SemSkip:  "(s,Skip ⟶⇩1 s" 
 SemAssign:"⟦ t = update s x (evalE e s)⟧ ⟹ s,(Assign x e) ⟶⇩1 t"
SemComp:  "⟦ s,c1 ⟶⇩n r; r,c2 ⟶⇩m t; k=(max n m)+1⟧
          ⟹ s,(Comp c1 c2) ⟶⇩k t"
 SemWhileT:"⟦evalB b s; s,c ⟶⇩n r; r,(While b c) ⟶⇩m t; 
             k=((max n m)+1)⟧
          ⟹ s,(While b c) ⟶⇩k t"
 SemWhileF:"⟦¬ (evalB b s); t=s⟧ ⟹ s,(While b c) ⟶⇩1 t"
 SemTrue:  "⟦evalB b s; s,c1 ⟶⇩n t⟧ ⟹ s,(Iff b c1 c2) ⟶⇩(n+1) t"
 SemFalse: "⟦¬ (evalB b s); s,c2 ⟶⇩n t⟧ 
          ⟹ s,(Iff b c1 c2) ⟶⇩(n+1) t"
 SemCall:  "⟦ s,body ⟶⇩n t⟧ ⟹ s,Call ⟶⇩(n+1) t"
*)

abbreviation
SemN  :: "[State, IMP, nat, State] ⇒ bool"   (‹ _ , _ →⇩_  _ ›)
where
"s,c →⇩n t == (s,c,n,t) : Semn"

text‹Often, the height index does not matter, so we define a notion
hiding it.›

definition Sem :: "[State, IMP, State] ⇒ bool" (‹_ , _ ⇓ _ › 1000)
where "s,c ⇓ t = (∃ n. s,c →⇩n t)"

text‹Inductive elimination rules for the (indexed) dynamic semantics:›

inductive_cases Sem_eval_cases: 
 "s,Skip →⇩n t"
 "s,(Assign x e) →⇩n t"
 "s,(Comp c1 c2) →⇩n t"
 "s,(While b c) →⇩n t"
 "s,(Iff b c1 c2) →⇩n t"
 "s, Call →⇩n t"

(*<*)
lemma Sem_no_zero_height_derivsAux: "∀ s t. ((s, c →⇩0 t) --> False)"
by (induct_tac c, auto elim: Sem_eval_cases)
(*>*)

text‹An induction on $c$ shows that no derivations of height
$0$ exist.›

lemma Sem_no_zero_height_derivs: "(s, c →⇩0 t) ==> False"
(*<*)by (insert Sem_no_zero_height_derivsAux, fastforce)(*>*)

(*<*)
lemma SemnDeterm[rule_format]:
"(s, c →⇩n t) ==> (∀ r m . (s, c →⇩m r) --> m=n ∧ r=t)"
apply (erule Semn.induct)
apply(clarsimp, elim Sem_eval_cases, simp)
(*Assign*)
apply (rule allI)+ apply rule
apply(elim Sem_eval_cases)
apply simp
(*Comp*)
apply (rule allI)+ apply rule
apply(elim Sem_eval_cases)
apply simp
(*WhileT*)
apply (rule allI)+ apply rule
apply (rotate_tac 3) apply (erule thin_rl)
apply (erule Sem_eval_cases) apply clarify
  apply (rotate_tac -4)
  apply (erule_tac x=rb in allE) apply (erule_tac x=na in allE) apply clarsimp 
  apply clarify
(*WhileF*)
apply (rule allI)+ apply rule
apply (erule Sem_eval_cases) apply clarify
  apply simp
(*True*)
apply (rule allI)+ apply rule
apply(elim Sem_eval_cases) 
apply simp
apply fast
(*False*)
apply (rule allI)+ apply rule
apply(elim Sem_eval_cases) 
apply fast
apply simp
(*Call*)
apply clarify
apply(elim Sem_eval_cases) 
apply simp
done
(*>*)

text‹The proof of determinism is by induction on the 
      (indexed) operational semantics.›

lemma SemDeterm: "⟦s, c ⇓ t; s, c ⇓ r⟧ ⟹ r=t"
(*<*)
apply (simp add: Sem_def, clarsimp)
apply (drule SemnDeterm, assumption)
apply simp
done
(*>*)

text‹End of theory IMP›
end