theory NikSmallStep
imports NikInstructions

begin

section \<open>Small steps operative semantics of Niklaus\<close>

text \<open>
  In small steps semantics, we define a relation between pairs of instructions and states.
  (i, s) and (i', s') are in relation if by executing instruction i in state s we reach
  state s' and still have to execute instruction i'.

  Defining a relation r amounts to defining a predicate that takes two arguments and returns:
  \<^item> True is the arguments are in relation
  \<^item> False is they are not

  Here, we use an inductive definition, which tells which pairs of (instruction, state)
  are in relation. We cannot use a function (see theory NikOpNaive) because we cannot
  prove its termination.
  The infix notation (i, s) \<rightarrow> (i', s'), which states that (i, s) and (i', s') are in relation,
  can be read as "executing i in state s leads in one step to executing i' in state s'".
\<close>
inductive small_step:: \<open>(instruction \<times> state) \<Rightarrow> (instruction \<times> state) \<Rightarrow> bool\<close> (infix \<open>\<rightarrow>\<close> 55)
where
  \<comment> \<open>These elementary instructions are executed in one step, so they lead in one step to Nop\<close>
  VDecl: \<open>(var v, s) \<rightarrow> (Nop, s(v:=0))\<close>
| Assign: \<open>(v <- val, s) \<rightarrow> (Nop, s(v:=evaluate val s))\<close>
  \<comment> \<open>Chaining a Nop with another instruction\<close>
| SeqNop: \<open>(Nop;; i, s) \<rightarrow> (i, s)\<close>
  \<comment> \<open>This one is more complex because instruction i may not be executable in one step\<close>
| Seq: \<open>(i, s) \<rightarrow> (z, s') \<Longrightarrow> (i;; j, s) \<rightarrow> (z;; j, s')\<close>
  \<comment> \<open>Two cases for if_then_else: when the condition is true and when the condition is false\<close>
| IfTrue: \<open>evalbool c s \<Longrightarrow> (if c then i1 else i2 fi, s) \<rightarrow> (i1, s)\<close>
| IfFalse: \<open>\<not>evalbool c s \<Longrightarrow> (if c then i1 else i2 fi, s) \<rightarrow> (i2, s)\<close>
  \<comment> \<open>While: when the condition is true, unroll the loop: execute the body, then the loop again\<close>
| WhileTrue: \<open>evalbool c s \<Longrightarrow> 
    (while c do body done, s) \<rightarrow> (body;; while c do body done, s)\<close>
  \<comment> \<open>While: when the condition is false, become a Nop\<close>
| WhileFalse: \<open>\<not>evalbool c s \<Longrightarrow>
    (while c do body done, s) \<rightarrow> (Nop, s)\<close>

text \<open>Generate standard ML code for this predicate\<close>
code_pred small_step .

text \<open>The following builds the set of all 'post' such as var ''x'' executed in one step leads to post\<close>
values \<open>{post. (var ''x'', \<lambda>x.0) \<rightarrow> post}\<close>
text \<open>
  Now, we look at the value of variables ''x'' and ''y'' in post. Since post = (instr, (env, input, output)),
  snd post is (env, input, output), and fst (snd post) is env. We use "map" to apply env to the list [''x'', ''y'']
  to get the value of varaibles x and y.
\<close>
values \<open>{map (snd post) [''x'', ''y'']|post. (var ''x'', \<lambda>x.0) \<rightarrow> post}\<close>

text \<open>Same thing to observe the result of x := 2\<close>
values \<open>{map (snd post) [''x'', ''y'']|post. (''x'' <- N 2, \<lambda>x.0) \<rightarrow> post}\<close>

text \<open>Here, we see that we execute only one step, so variable y is not yet modified in the result\<close>
values \<open>{post. (''x'' <- N 2 ;; ''y'' <- V ''x'', \<lambda>x.0) \<rightarrow> post}\<close>
values \<open>{map (snd post) [''x'', ''y'']|post. (''x'' <- N 2 ;; ''y'' <- V ''x'', \<lambda>x.0) \<rightarrow> post}\<close>

subsection \<open>Chaining small steps\<close>
text \<open>
  We want to compute the behavior of a program as (i, s) \<rightarrow> (i2, s2) \<rightarrow> (i3, s3) ... \<rightarrow> (i', s')
  For this, we need to define the reflexive transitive closure of \<rightarrow> 
\<close>
text \<open>Reflexive transitive closure of a relation\<close>
inductive star :: \<open>('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)\<close>
for r where  \<comment> \<open>relation r is fixed in this definition\<close>
    refl: \<open>(star r) x x\<close>   \<comment> \<open>star r is reflexive\<close>
  | trans: \<open>\<lbrakk>r x y ; (star r) y z\<rbrakk> \<Longrightarrow> (star r) x z\<close> \<comment> \<open>star r closes r by transitivity\<close>

text \<open>Hide rules refl and trans because they have too generic names which may create conflicts\<close>
hide_fact (open) refl trans

thm star.induct
print_statement star.induct

text \<open>Show that star r is transitive\<close>
lemma star_trans: \<open>\<lbrakk>(star r) x y ; (star r) y z\<rbrakk> \<Longrightarrow> (star r) x z\<close>
(* by (induction rule:star.induct, (simp add: star.trans)+) *)
proof (induction rule:star.induct)
  \<comment> \<open>(star r x z) if either x = z (star.refl), so we have (star r) x z, done\<close>
  case (refl x) thus ?case .
next
  \<comment> \<open>or r x y and (star r) y za (star.trans).
     With (star r) za z, we get (star r) y z (by IH)
     and with r x y and (star r) y z we get (star r) x z, done\<close>
  case (trans x y za) print_facts
    from \<open>star r za z\<close> and trans.IH have \<open>star r y z\<close> by simp
    with \<open>r x y\<close> show ?case by (rule star.trans)
qed

lemma \<open>\<lbrakk>(star r) x y ; (star r) y z\<rbrakk> \<Longrightarrow> (star r) x z\<close>
apply (induction rule:star.induct)
apply (assumption)
apply (erule star.trans)
apply simp
done

text \<open>
  star.induct works only for r x y.
  Here, we build a version of the induction theorem for relations on
  tuplets, like: r (i, pre) (i', post), for it to work with small_step
\<close>
thm star.induct
lemmas star_induct =
  star.induct[of \<open>r:: 'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool\<close>, split_format(complete)]

text \<open>For proof automation, make reflexivity of star a simplification and an introduction rule\<close>
thm star.refl
declare star.refl[simp,intro]

text \<open>Make this obvious fact a simplification and introduction rule\<close>
lemma star_trans1[simp, intro]: \<open>r x y \<Longrightarrow> (star r) x y\<close>
(* by (simp add: star.trans) *)
proof -
  assume 1: \<open>r x y\<close>
  moreover have \<open>(star r) y y\<close> using star.refl .
  ultimately show ?thesis by (simp add: star.trans)
qed

text \<open>Generate code for star\<close>
code_pred star .

text \<open>
  We can now define small_steps as the reflexive transitive closure of small_step
  We note (i, s) \<rightarrow>* (i', s') the fact that we can go in several steps 
  from (i, s) to (i', s')
\<close>
abbreviation small_steps :: 
  \<open>instruction \<times> state \<Rightarrow> instruction \<times> state \<Rightarrow> bool\<close> (infix \<open>\<rightarrow>*\<close> 55)
where \<open>small_steps pre post \<equiv> (star small_step) pre post\<close>

text \<open>
  schematic_goal introduces a goal with schematic variables.
  Here, we use the proof of a schematic goal to compute the result
  of executing "x := 2; y = x" in an empty environment.
\<close>
schematic_goal \<open>(''x'' <- N 2 ;; ''y'' <- V ''x'', \<lambda>x.0) \<rightarrow>* ?post\<close>
apply (rule star.trans)  \<comment> \<open>force the execution of one step\<close>
apply (rule Seq)         \<comment> \<open>apply the Seq rule to go to the first instruction\<close>
apply (rule Assign)      \<comment> \<open>apply the Assign rule to handle it\<close>
apply simp               \<comment> \<open>simplify to get the computed value of x\<close>
apply (rule star.trans)  \<comment> \<open>go to the next step\<close>
apply (rule SeqNop)      \<comment> \<open>get rid of the Nop we got when stepping through the assignment\<close>
apply (rule star.trans)  \<comment> \<open>go to the next step\<close>
apply (rule Assign)      \<comment> \<open>apply the Assign rule to handle it\<close>
apply simp               \<comment> \<open>simplify to get the computed value of y\<close>
apply (rule star.refl)   \<comment> \<open>apply the reflexivity rule to finish and get ?post\<close>
done
text \<open>so we can see that at the end, we have x and y = 2\<close>

text \<open>
  Here, we use the generated ML code to compute the set of 
  (i', s') (we look only at the value of x and y in each s')
  that can be reached through big steps.
\<close>
values \<open>{map (snd post) [''x'', ''y'']
  |post. (''x''<-(N 3);; ''y''<-(V ''x''), \<lambda>x.0) \<rightarrow>* post}\<close>
text \<open>
  We get them in order:
    [0, 0] is reached in 0 steps (because of reflexivity)
    [3, 0] is reached after executing x := 3 (with Nop as next instruction)
    [3, 0] is reached after executing the Nop to which x:=3 led
    [3, 3] is reached after executing y := x (leading to a Nop)
\<close>

text \<open>
  In order to automatically prove the next theorem, we need to 
  give some information to the automatic proof methods.
  Elimination rules allow these methods to transform facts
  into simpler facts. For instance P \<and> Q can be transformed
  into facts P and Q by eliminating \<and> (this is rule conjE).
  Since we defined \<rightarrow> as an inductive predicate, the inductive_cases
  command allows us to generate these rules automatically. We just 
  have to state that they should be used as elimination rules with 
  the [elim] attribute. [elim!] says that the rule can be used as
  much as possible. For the while loop, we use [elim] because
  "as much as possible" would be an infinite number of times!
  There is a "thm" statement after each generation so that you
  can easily have a look at the form of these rules.
\<close>
text \<open>Rule inversion\<close>
inductive_cases NopE[elim!]: \<open>(Nop, pre) \<rightarrow> cont\<close>
thm NopE
inductive_cases VDeclE[elim!]: \<open>(var x, s) \<rightarrow> (i, s')\<close>
thm VDeclE
inductive_cases AssignE[elim!]: \<open>(x <- e, s) \<rightarrow> (i, s')\<close>
thm AssignE
inductive_cases SeqNopE[elim!]: \<open>(Nop;; i2, s) \<rightarrow> (i, s')\<close>
thm SeqNopE
inductive_cases SeqE[elim!]: \<open>(i1;; i2, pre) \<rightarrow> cont\<close>
thm SeqE
inductive_cases AltE[elim!]: \<open>(if c then iT else iF fi, s) \<rightarrow> (i, s')\<close>
thm AltE
inductive_cases WhileE[elim]: \<open>(while c do body done, s) \<rightarrow> (i, s')\<close>
thm WhileE

text \<open>
  Prove that the small step semantics is deterministic:
  a given instruction executed in a given state always leads to the same state.
\<close>
theorem small_step_deterministic:
  \<open>\<lbrakk>pre \<rightarrow> post; pre \<rightarrow> post'\<rbrakk> \<Longrightarrow> post' = post\<close>
by (induction arbitrary: post' rule: small_step.induct, auto)

end