header {* Assessed Exercise II: Semantics*}

(*<*) theory semantics_ex imports Main begin (*>*)

text {* This assessed exercise continues the proofs concerning
operational semantics that were outlined in the lectures. Please
deliver the completed exercise and theory file by the appropriate
deadline.*}

subsection {* Syntax and Semantics of Commands*}

text {*As in the lectures, the theory begins by specifying the types of
locations, values (here we use the natural numbers), states, and
finally arithmetic and boolean expressions. *}

typedecl loc 
  -- "an unspecified (arbitrary) type of locations 
      (adresses/names) for variables"

types 
  val   = nat -- "or anything else, @{text nat} used in examples"
  state = "loc \<Rightarrow> val"
  aexp  = "state \<Rightarrow> val"  
  bexp  = "state \<Rightarrow> bool"
  -- "arithmetic and boolean expressions are not modelled explicitly here,"
  -- "they are just functions on states"

text {* The commands include SKIP, which does nothing, assignments,
sequencing, conditionals and repetition. Note: our use of the
semicolon character for sequencing could cause syntactic ambiguities
if you attempt to use the semicolons to separate the preconditions of
theorems. You can instead express properties using the symbol @{text
\<Longrightarrow>}. *}

datatype
  com = SKIP                    
      | Assign loc aexp         (infixr ":==" 80)
      | Semi   com com          (infixr ";" 70)
      | Cond   bexp com com     ("IF _ THEN _ ELSE _"  [0, 90, 90] 91)
      | While  bexp com         ("WHILE _ DO _" [0, 91] 90)

text {* The big-step execution relation @{text evalc} is defined
inductively, as in the lectures. *}

inductive
  evalc :: "[com,state,state] \<Rightarrow> bool" ("\<langle>_, _\<rangle>/ \<leadsto> _" [0,0,60] 60)
where
  Skip:    "\<langle>SKIP,s\<rangle> \<leadsto> s"
| Assign:  "\<langle>x :== a,s\<rangle> \<leadsto> s(x := a s)"

| Semi:    "\<langle>c0,s\<rangle> \<leadsto> s'' \<Longrightarrow> \<langle>c1,s''\<rangle> \<leadsto> s' \<Longrightarrow> \<langle>c0; c1, s\<rangle> \<leadsto> s'"

| IfTrue:  "b s \<Longrightarrow> \<langle>c0,s\<rangle> \<leadsto> s' \<Longrightarrow> \<langle>IF b THEN c0 ELSE c1, s\<rangle> \<leadsto> s'"
| IfFalse: "\<not>b s \<Longrightarrow> \<langle>c1,s\<rangle> \<leadsto> s' \<Longrightarrow> \<langle>IF b THEN c0 ELSE c1, s\<rangle> \<leadsto> s'"

| WhileFalse: "\<not>b s \<Longrightarrow> \<langle>WHILE b DO c,s\<rangle> \<leadsto> s"
| WhileTrue:  "b s \<Longrightarrow> \<langle>c,s\<rangle> \<leadsto> s'' \<Longrightarrow> \<langle>WHILE b DO c, s''\<rangle> \<leadsto> s'
               \<Longrightarrow> \<langle>WHILE b DO c, s\<rangle> \<leadsto> s'"

text {*Next come commands that set up Isabelle's automation. The rules
that make up the inductive definition can be used as introduction
rules, and rule inversion from the definition supplies us with
elimination rules. This again is very similar to the material in the
lectures. *}

lemmas evalc.intros [intro] -- "use those rules in automatic proofs"

inductive_cases skipE [elim!]:   "\<langle>SKIP,s\<rangle> \<leadsto> s'"
inductive_cases semiE [elim!]:   "\<langle>c0; c1, s\<rangle> \<leadsto> s'"
inductive_cases assignE [elim!]: "\<langle>x :== a,s\<rangle> \<leadsto> s'"
inductive_cases ifE [elim!]:     "\<langle>IF b THEN c0 ELSE c1, s\<rangle> \<leadsto> s'"
inductive_cases whileE [elim]:   "\<langle>WHILE b DO c,s\<rangle> \<leadsto> s'"

subsection {*Equivalence of commands*}

text{*Two commands are equivalent if they allow the same transitions.*}

definition
  equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" (infixr "\<sim>" 60)
where
  "(c \<sim> c') = (\<forall>s s'. (\<langle>c, s\<rangle> \<leadsto> s') = (\<langle>c', s\<rangle> \<leadsto> s'))"

text {* The following rule of inference, made available to Isabelle's
automatic methods as an introduction rule, allows us to prove semantic
equivalence statements. This again was covered in the lectures. *}

lemma equivI [intro!]:
  "(\<And>s s'. \<langle>c, s\<rangle> \<leadsto> s' = \<langle>c', s\<rangle> \<leadsto> s') \<Longrightarrow> c \<sim> c'"
(*<*)by (auto simp add: equiv_c_def)(*>*)

text {* \begin{task}Prove the following theorem. \end{task} 
*}
lemma equiv_if3:
  "c1 \<sim> c2 \<Longrightarrow> 
   (IF b1 THEN c1 ELSE IF b2 THEN c2 ELSE c3) \<sim> 
   (IF b2 THEN c2 ELSE IF b1 THEN c1 ELSE c3)" 
(*<*)oops(*>*)


text {*  \begin{task}
  Prove the following theorem, which establishes that semantic
  equivalence is a congruence relation with respect to @{text
  While}. Unlike analogous proofs for other constructors, this proof
  requires a lemma proved by induction.
  \end{task} 
*}
lemma equiv_while:
  "c \<sim> c' \<Longrightarrow> (WHILE b DO c) \<sim> (WHILE b DO c')"
(*<*)oops(*>*)

text {*  \begin{task}
Prove the following theorem, which expresses that the
Boolean expression guarding the loop holds at the start of the loop
body.\end{task}  
*}
lemma equiv_while_if:
  "(WHILE b1 DO IF b2 THEN c1 ELSE c2) \<sim> 
   (WHILE b1 DO IF (\<lambda>s. b1 s & b2 s) THEN c1 ELSE c2)"
(*<*)oops(*>*)


subsection{*A Command Preserves a Boolean Expression*}

(*<*)consts
  preserves :: "com \<Rightarrow> bexp \<Rightarrow> bool"
(*>*)

text {* The following two properties allow a command @{text c} to be
moved out of a conditional command. One of them can be proved as shown.
The other one can be proved subject to the precondition
@{text "preserves c b"}, which expresses that the command @{text c}
preserves the value of the Boolean expression @{text b}. 

 \begin{task}
Formalise the concept @{text "preserves c b"} in Isabelle, and prove
both properties in the appropriate form.\end{task} *}

lemma equiv_if1:
  "(IF b THEN (c; c1) ELSE (c; c2)) \<sim> (c; (IF b THEN c1 ELSE c2))" 
(*<*)oops(*>*)

lemma equiv_if2:
  "(IF b THEN (c1; c) ELSE (c2; c)) \<sim> ((IF b THEN c1 ELSE c2); c)" 
(*<*)oops(*>*)

(*<*) end (*>*)