(*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
 . Syntax and operational semantics are as in cite‹"Winskel93"›,
  that we enrich the language with a single unnamed,
  procedure. Both, this section and the following one
  set the basis for the development described in the later
  and largely follow the approach to formalize program logics
  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
 .›

typedecl Var
typedecl Val

text‹Arithmetic expressions are inductively built up from variables,
 , and binary operators which are modeled as meta-logical
  over values. Similarly, boolean expressions are built up
  arithmetic expressions using binary boolean operators which are
  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
  $\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
 .›

consts body :: IMP

subsection‹Dynamic semantics›

text‹States are given by stores - in our case, HOL functions
  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
 .›

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
  height index that facilitates the Kleymann-Nipkow-style~cite‹"KleymannPhD" and "Nipkow-CSL02"›
  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 \<longrightarrow>\<^sub>1 s" 
 SemAssign:"\<lbrakk> t = update s x (evalE e s)\<rbrakk> \<Longrightarrow> s,(Assign x e) \<longrightarrow>\<^sub>1 t"
SemComp:  "\<lbrakk> s,c1 \<longrightarrow>\<^sub>n r; r,c2 \<longrightarrow>\<^sub>m t; k=(max n m)+1\<rbrakk>
          \<Longrightarrow> s,(Comp c1 c2) \<longrightarrow>\<^sub>k t"
 SemWhileT:"\<lbrakk>evalB b s; s,c \<longrightarrow>\<^sub>n r; r,(While b c) \<longrightarrow>\<^sub>m t; 
             k=((max n m)+1)\<rbrakk>
          \<Longrightarrow> s,(While b c) \<longrightarrow>\<^sub>k t"
 SemWhileF:"\<lbrakk>\<not> (evalB b s); t=s\<rbrakk> \<Longrightarrow> s,(While b c) \<longrightarrow>\<^sub>1 t"
 SemTrue:  "\<lbrakk>evalB b s; s,c1 \<longrightarrow>\<^sub>n t\<rbrakk> \<Longrightarrow> s,(Iff b c1 c2) \<longrightarrow>\<^sub>(n+1) t"
 SemFalse: "\<lbrakk>\<not> (evalB b s); s,c2 \<longrightarrow>\<^sub>n t\<rbrakk> 
          \<Longrightarrow> s,(Iff b c1 c2) \<longrightarrow>\<^sub>(n+1) t"
 SemCall:  "\<lbrakk> s,body \<longrightarrow>\<^sub>n t\<rbrakk> \<Longrightarrow> s,Call \<longrightarrow>\<^sub>(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
  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 →₀ 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 →₀ 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