Sémantique opérationnelle à grands pas
Approche naïve
Essayez tout d'abord de compléter la théorie suivante, qui tente naïvement de définir la sémantique opérationnelle de Niklaus à l'aide d'une fonction.
NikOpNaiveExercise.thy (:brush=isabelle:) theory NikOpNaiveExercise imports NikInstructions
begin section ‹Naïve attempt at an operational semantics›
text ‹
Naïve attempt to define the semantics of the instructions using a recursive function.
› fun execute:: ‹instruction ⇒ state ⇒ state› where
‹execute Nop s = s› | ‹execute (var v) s = s(v:=0)› ― ‹Other cases...›
end (:endbrush:)
Utilisation d'un prédicat inductif
Exercice
NikBigStepExercise.thy (:brush=isabelle:) theory NikBigStepExercise imports NikInstructions
begin section ‹Big step operative semantics of Niklaus›
text ‹
In big step semantics, we define a relation between a pair (instruction, state) and the state reached after executing the instruction from the original state. (i, s) and s' are in relation if by executing instruction i in state s we reach state s'. Defining a relation r amounts to defining a predicate that takes two arguments and returns: ▪ True is the arguments are in relation ▪ False is they are not Here, we use an inductive definition, which tells which pairs of (instruction, state) and state are in relation. We cannot use a function (see theory NikInstructions) because we cannot prove its termination. The infix notation (i, s) ↝ s', which states that (i, s) and s' are in relation, can be read as ‹executing i in state s leads to state s'›.
› inductive big_step :: ‹(instruction × state) ⇒ state ⇒ bool› (infix ‹↝› 55) where
Nop: ‹(Nop, s) ↝ s› | VDecl: ‹(var v, s) ↝ s(v:=0)› | Assign: ―‹FIX ME› ‹(v <- e, s)↝s'› | Seq: ‹⟦(i1, s) ↝ s'; (i2, s') ↝ s''⟧ ⟹ (i1;; i2, s) ↝ s''› | IfTrue: ―‹FIX ME› ‹(ifte, s)↝s'› | IfFalse: ―‹FIX ME› ‹(ifte, s)↝s'› | WhileFalse: ―‹FIX ME› ‹(wh, s)↝s'› | WhileTrue: ―‹FIX ME› ‹(wh, s)↝s'›
print_theorems
text ‹Some proofs to check that this works properly›
text ‹P[of t1 t2 ... tn] substitutes t1, t2, ... tn to the n first schematic variables of P› thm VDecl thm VDecl[of ‹x› ‹s›] thm VDecl[where v=‹x› and s=‹s›]
lemma ‹(var x, s) ↝ s(x := 0)› by (rule VDecl[of ‹x› ‹s›])
text ‹The same lemma, but we let the unifier find substitutions› lemma ‹(var x, s) ↝ s(x := 0)› by (rule VDecl)
text ‹We can even let Isabelle find the rule by itself...› lemma ‹(var x, s) ↝ s(x := 0)› ..
text ‹An auxilliary lemma to help with the assignment of constants› lemma AssignConst: ‹(v <- N n, s) ↝ s(v := n)›
using Assign[where e=‹N n›] by simp
lemma ‹(x <- N 3, s) ↝ s(x := 3)› ― ‹Here, we cannot apply the Assign rule directly, because this rule expects
a term in the form ‹evaluate e pre›. We use AssignConst instead:› apply (rule AssignConst)
done
text ‹
In a schematic goal, schematic variables will be determined during the proof. Here, we will find the final state ?s'
› schematic_goal ex1: ― ‹use schematic_lemma in versions of Isabelle before 2016›
‹(x <- N 3 ;; y <- V x, s) ↝ ?s'›
― ‹Applying the Seq rule goes backward to the premisses of the lemma› apply (rule Seq) ― ‹The Assign rule discharges the first premisse› apply (rule AssignConst) ― ‹The Assign rule discharges the second premisse› apply (rule Assign) done text ‹
?s' was determined during this proof, we can get its value in the simplified form of the lemma
› thm ex1 thm ex1[simplified]
text ‹Computing the GCD of 2 and 3 by successive subtractions› text ‹To avoid to much copy-pasting, we define an abbreviation› abbreviation ‹GCD_2_3 ≡ a <- N 2 ;; b <- N 3 ;;
while V a .≠. V b do if V a .<. V b then b <- V b .-. V a else a <- V a .-. V b fi done
› text ‹Manual solving by invoking the right rule at each step:› schematic_goal gcd2_3: ‹(GCD_2_3, λx.0) ↝ ?s›
sorry
thm gcd2_3
text ‹Generate code for predicate big_step› code_pred big_step .
text ‹
Compute the result of a program using this generated code. The "values" command find all the values that belong to the comprehension set given as argument. Here, it will give us the set of states that are in relation with ‹(GCD_2_3, λx.0)›, i.e. the set of the states that can be reached from a state in which all variables are 0 by executing the GCD_2_3 program. Since Niklaus is a deterministic language, there is only one such state, in whi bothe a and b have value 1.
›
values ‹{res. (GCD_2_3, λx.0) ↝ res }›
text ‹Use map to display the value of a and b in the environment of the result› values ‹{map res [a, b]|res. (GCD_2_3, λx.0) ↝ res }›
end (:endbrush:)
Corrigé
NikBigStep.thy (:brush=isabelle:) theory NikBigStep imports NikInstructions
begin section ‹Big step operative semantics of Niklaus›
text ‹
In big step semantics, we define a relation between a pair (instruction, state) and the state reached after executing the instruction from the original state. (i, s) and s' are in relation if by executing instruction i in state s we reach state s'. Defining a relation r amounts to defining a predicate that takes two arguments and returns: ▪ True is the arguments are in relation ▪ False is they are not Here, we use an inductive definition, which tells which pairs of (instruction, state) and state are in relation. We cannot use a function (see theory NikInstructions) because we cannot prove its termination. The infix notation (i, s) ↝ s', which states that (i, s) and s' are in relation, can be read as "executing i in state s leads to state s'".
› inductive big_step :: "(instruction × state) ⇒ state ⇒ bool" (infix "↝" 55) where
Nop: "(Nop, s) ↝ s" | VDecl: "(var v, s) ↝ s(v:=0)" | Assign: "(v <- e, s) ↝ s(v:=evaluate e s)" | Seq: "⟦(i1, s) ↝ s'; (i2, s') ↝ s''⟧ ⟹ (i1;; i2, s) ↝ s''"
― ‹Cas du if then else avec condition vraie: on exécute i1›
| IfTrue: "⟦evalbool c s ; (i1, s) ↝ s'⟧ ⟹ (if c then i1 else i2 fi, s) ↝ s'"
― ‹Cas du if then else avec condition false: on exécute i2›
| IfFalse: "⟦¬evalbool c s ; (i2, s) ↝ s'⟧ ⟹ (if c then i1 else i2 fi, s) ↝ s'"
― ‹Cas du while avec condition fausse: on ne change pas d'état›
| WhileFalse: "¬evalbool c s ⟹ (while c do body done, s) ↝ s"
― ‹Cas du while avec condition vraie: on déroule un tour de boucle›
| WhileTrue: "⟦evalbool c s; (body, s) ↝ s'; (while c do body done, s') ↝ s''⟧ ⟹ (while c do body done, s) ↝ s''"
print_theorems
text ‹Some proofs to check that this works properly›
text ‹P[of t1 t2 ... tn] substitutes t1, t2, ... tn to the n first schematic variables of P› thm VDecl thm VDecl[of "x" "s"] thm VDecl[where v="x" and s="s"]
lemma "(var x, s) ↝ s(x := 0)" by (rule VDecl[of "x" "s"])
text ‹The same lemma, but we let the unifier find substitutions› lemma "(var x, s) ↝ s(x := 0)" by (rule VDecl)
text ‹We can even let Isabelle find the rule by itself...› lemma "(var x, s) ↝ s(x := 0)" ..
text ‹An auxilliary lemma to help with the assignment of constants› lemma AssignConst: ‹(v <- N n, s) ↝ s(v := n)› proof -
have "evaluate (N n) s = n" by simp with Assign[where e=‹N n›] show ?thesis by simp
qed
thm Assign lemma "(x <- N 3, s) ↝ s(x := 3)" ― ‹Here, we cannot apply the Assign rule directly, because this rule expects
a term in the form "evaluate e pre". We use AssignConst instead:› apply (rule AssignConst)
done
text ‹
In a schematic goal, schematic variables will be determined during the proof. Here, we will find the final state ?s'
› schematic_goal ex1: ― ‹use schematic_lemma in versions of Isabelle before 2016›
"(x <- N 3 ;; y <- V x, s) ↝ ?s'"
― ‹Applying the Seq rule goes backward to the premisses of the lemma› apply (rule Seq) ― ‹The Assign rule discharges the first premisse› apply (rule Assign) ― ‹simp simplifies evaluate (N 3) s› apply (simp) ― ‹The Assign rule discharges the second premisse› apply (rule Assign) done text ‹
?s' was determined during this proof, we can get its value in the simplified form of the lemma
› thm ex1 thm ex1[simplified]
text ‹Computing the GCD of 2 and 3 by successive subtractions› schematic_goal gcd2_3: " (a<- N 2;; b<- N 3;;
while V a .≠. V b do if V a .<. V b then b<- V b .-.V a else a<- V a .-. V b fi done, λx.0) ↝ ?s
"
apply (rule Seq) apply (rule AssignConst) apply (rule Seq) apply (rule AssignConst) apply (rule WhileTrue) apply simp apply (rule IfTrue) apply simp apply (rule Assign) apply simp apply (rule WhileTrue) apply simp apply (rule IfFalse) apply simp apply (rule Assign) apply simp apply (rule WhileFalse) apply simp done
thm gcd2_3
text ‹To avoid to much copy-pasting, we define an abbreviation› abbreviation "GCD_2_3 ≡ a <- N 2 ;; b <- N 3 ;;
while V a .≠. V b do if V a .<. V b then b <- V b .-. V a else a <- V a .-. V b fi done
"
text ‹Generate code for predicate big_step› code_pred big_step .
text ‹Compute the result of a program using this generated code› values "{res. (GCD_2_3, λx.0) ↝ res }"
text ‹Use map to display the value of a and b in the environment of the result› values "{map res [a, b]|res. (GCD_2_3, λx.0) ↝ res }"
end (:endbrush:)
Propriétés de la sémantique (et du langage)
Il est possible de définir la notion d'instructions équivalentes, qui peut être utile par exemple pour prouver la correction d'un optimiseur de code.
On démontre également que le langage Niklaus est déterministe : lorsqu'on exécute une instruction à partir d'un état de la machine, on arrive toujours dans un seul état.
NikBigStepProperties.thy (:brush=isabelle:) theory NikBigStepProperties
imports NikBigStep
begin
text ‹Equivalence of instructions› abbreviation equiv_instr :: ‹instruction ⇒ instruction ⇒ bool› where ‹equiv_instr i1 i2 ≡ (∀ pre post. (i1, pre) ↝ post = (i2, pre) ↝ post)›
text ‹Proof automation› thm big_step.intros declare big_step.intros [intro] thm big_step.induct ― ‹Standard induction rule› text ‹Allow splitting the (instruction, state) in lemmas› lemmas big_step_induct = big_step.induct[split_format(complete)] thm big_step_induct
text ‹Rule inversion› inductive_cases NopElim[elim!]: ‹(Nop, s) ↝ s'› thm NopElim inductive_cases VDeclElim[elim!]: ‹(var x, s) ↝ s'› thm VDeclElim inductive_cases AssignElim[elim!]: ‹(x <- e, s) ↝ s'› thm AssignElim inductive_cases SeqElim[elim!]: ‹(i1;; i2, s) ↝ s'› thm SeqElim inductive_cases AltElim[elim!]: ‹(if c then i1 else i2 fi, s) ↝ s'› thm AltElim inductive_cases WhileElim[elim]: ‹(while c do body done, s) ↝ s'› thm WhileElim
lemma ‹(if c then Nop else Nop, pre) ↝ post ⟹ pre = post› by auto
lemma ‹equiv_instr (if c then i else i fi) i› by auto
lemma unfold_while:
‹equiv_instr (while cond do body done) (if cond then body;; while cond do body done else Nop fi)›
by auto
text ‹Prove that the big step semantics is deterministic› lemma Nik_deterministic: ‹⟦ (prog, s) ↝ s';
(prog, s) ↝ s''⟧ ⟹ s'' = s'›
by (induction arbitrary: s'' rule: big_step_induct, blast+)
text ‹More detailed proof: we give some hints about why it is true in the different cases› lemma Nik_deterministic2: ‹⟦ (prog, s) ↝ s';
(prog, s) ↝ s'' ⟧ ⟹ s'' = s'›
proof (induction arbitrary: s'' rule: big_step_induct)
print_cases case Nop thus ?case by (rule NopElim)
next
case VDecl thus ?case by (rule VDeclElim)
next
case Assign thus ?case by (rule AssignElim)
next
case Seq print_facts thm SeqElim Seq.prems SeqElim[OF Seq.prems] Seq.IH(1) SeqElim[OF Seq.prems, OF Seq.IH(1)] thm SeqElim Seq.prems SeqElim[OF Seq.prems] Seq.IH(2) SeqElim[OF Seq.prems, OF Seq.IH(2)] from SeqElim[OF Seq.prems, OF Seq.IH(1)] and SeqElim[OF Seq.prems, OF Seq.IH(2)] show ?case by simp
next
case IfTrue print_facts from AltElim[OF IfTrue.prems, OF IfTrue.IH] show ?case by (simp add: IfTrue(1))
next
case IfFalse print_facts from AltElim[OF IfFalse.prems, OF IfFalse.IH] show ?case by (simp add: IfFalse(1,3,4))
next
case WhileFalse print_facts show ?case using WhileFalse.hyps WhileFalse.prems by blast
next
case WhileTrue print_facts show ?case using WhileTrue.IH WhileTrue.hyps(1) WhileTrue.prems by blast
qed
text ‹Very detailed proof, almost like on the blackboard.› lemma Nik_deterministic3: ‹⟦ (prog, s) ↝ s';
(prog, s) ↝ s'' ⟧ ⟹ s'' = s'›
proof (induction arbitrary: s'' rule: big_step.induct[split_format(complete)])
print_cases case (Nop pre) from ‹(Nop, pre) ↝ s› show ‹s = pre› by (rule NopElim)
next
case (VDecl v pre) from ‹(var v, pre) ↝ s› show ‹s = pre(v := 0)› by (rule VDeclElim)
next
case (Assign v e pre) from ‹(v <- e, pre) ↝ s› show ‹s = pre(v := evaluate e pre)› by (rule AssignElim)
next
case (Seq i1 pre p' i2 post) from ‹(i1 ;; i2, pre) ↝ s› have ‹∃q. (i1, pre) ↝ q ∧ (i2, q) ↝ s› by blast then obtain q where q1:‹(i1, pre) ↝ q› and q2:‹(i2, q) ↝ s''› by blast from q1 and Seq.IH(1) have ‹q = p'› by simp with q2 and Seq.IH(2) show ‹s'' = post› by simp
next
case (IfTrue c pre i1 post i2) print_facts from ‹(if c then i1 else i2 fi, pre) ↝ s› and ‹evalbool c pre› have ‹(i1, pre) ↝ s› by blast with IfTrue.IH show ‹s'' = post› .
next
case (IfFalse c pre i2 post i1) from ‹(if c then i1 else i2 fi, pre) ↝ s› and ‹¬ evalbool c pre› have ‹(i2, pre) ↝ s› by blast with IfFalse.IH show ‹s'' = post› .
next
case (WhileFalse c pre body) print_facts from ‹(while c do body done, pre) ↝ s› and ‹¬ evalbool c pre› show ‹s = pre› by blast
next
case (WhileTrue c pre body p' post) print_facts from ‹(while c do body done, pre) ↝ s''› and ‹evalbool c pre› have ‹∃q. (body, pre) ↝ q ∧ (while c do body done, q) ↝ s''› by blast then obtain q where q1:‹(body, pre) ↝ q› and q2:‹(while c do body done, q) ↝ s''› by blast from q1 and WhileTrue.IH(1) have ‹q = p'› by simp with q2 and WhileTrue.IH(2) show ‹s'' = post› by simp
qed
end (:endbrush:)
Sémantique à petits pas
Pour ceux qui sont intéressés, voici une version à petits pas de la sémantique opérationnelle de Niklaus, qui ne sera pas abordée en cours.
NikSmallStep.thy (:brush=isabelle:) theory NikSmallStep imports NikInstructions
begin
section ‹Small steps operative semantics of Niklaus›
text ‹
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: ▪ True is the arguments are in relation ▪ 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) → (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'".
› inductive small_step:: ‹(instruction × state) ⇒ (instruction × state) ⇒ bool› (infix ‹→› 55) where
― ‹These elementary instructions are executed in one step, so they lead in one step to Nop› VDecl: ‹(var v, s) → (Nop, s(v:=0))›
| Assign: ‹(v <- val, s) → (Nop, s(v:=evaluate val s))›
― ‹Chaining a Nop with another instruction›
| SeqNop: ‹(Nop;; i, s) → (i, s)›
― ‹This one is more complex because instruction i may not be executable in one step›
| Seq: ‹(i, s) → (z, s') ⟹ (i;; j, s) → (z;; j, s')›
― ‹Two cases for if_then_else: when the condition is true and when the condition is false›
| IfTrue: ‹evalbool c s ⟹ (if c then i1 else i2 fi, s) → (i1, s)› | IfFalse: ‹¬evalbool c s ⟹ (if c then i1 else i2 fi, s) → (i2, s)›
― ‹While: when the condition is true, unroll the loop: execute the body, then the loop again›
| WhileTrue: ‹evalbool c s ⟹
(while c do body done, s) → (body;; while c do body done, s)› ― ‹While: when the condition is false, become a Nop›
| WhileFalse: ‹¬evalbool c s ⟹
(while c do body done, s) → (Nop, s)›
text ‹Generate standard ML code for this predicate› code_pred small_step .
text ‹The following builds the set of all 'post' such as var x executed in one step leads to post› values ‹{post. (var x, λx.0) → post}› text ‹
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.
› values ‹{map (snd post) [x, y]|post. (var x, λx.0) → post}›
text ‹Same thing to observe the result of x := 2› values ‹{map (snd post) [x, y]|post. (x <- N 2, λx.0) → post}›
text ‹Here, we see that we execute only one step, so variable y is not yet modified in the result› values ‹{post. (x <- N 2 ;; y <- V x, λx.0) → post}› values ‹{map (snd post) [x, y]|post. (x <- N 2 ;; y <- V x, λx.0) → post}›
subsection ‹Chaining small steps› text ‹
We want to compute the behavior of a program as (i, s) → (i2, s2) → (i3, s3) ... → (i', s') For this, we need to define the reflexive transitive closure of →
› text ‹Reflexive transitive closure of a relation› inductive star :: ‹('a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool)› for r where ― ‹relation r is fixed in this definition›
refl: ‹(star r) x x› ― ‹star r is reflexive› | trans: ‹⟦r x y ; (star r) y z⟧ ⟹ (star r) x z› ― ‹star r closes r by transitivity›
text ‹Hide rules refl and trans because they have too generic names which may create conflicts› hide_fact (open) refl trans
thm star.induct print_statement star.induct
text ‹Show that star r is transitive› lemma star_trans: ‹⟦(star r) x y ; (star r) y z⟧ ⟹ (star r) x z› (* by (induction rule:star.induct, (simp add: star.trans)+) *) proof (induction rule:star.induct)
― ‹(star r x z) if either x = z (star.refl), so we have (star r) x z, done› case (refl x) thus ?case .
next
― ‹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› case (trans x y za) print_facts from ‹star r za z› and trans.IH have ‹star r y z› by simp with ‹r x y› show ?case by (rule star.trans)
qed
lemma ‹⟦(star r) x y ; (star r) y z⟧ ⟹ (star r) x z› apply (induction rule:star.induct) apply (assumption) apply (erule star.trans) apply simp done
text ‹
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
› thm star.induct lemmas star_induct =
star.induct[of ‹r:: 'a × 'b ⇒ 'a × 'b ⇒ bool›, split_format(complete)]
text ‹For proof automation, make reflexivity of star a simplification and an introduction rule› thm star.refl declare star.refl[simp,intro]
text ‹Make this obvious fact a simplification and introduction rule› lemma star_trans1[simp, intro]: ‹r x y ⟹ (star r) x y› (* by (simp add: star.trans) *) proof -
assume 1: ‹r x y› moreover have ‹(star r) y y› using star.refl . ultimately show ?thesis by (simp add: star.trans)
qed
text ‹Generate code for star› code_pred star .
text ‹
We can now define small_steps as the reflexive transitive closure of small_step We note (i, s) →* (i', s') the fact that we can go in several steps from (i, s) to (i', s')
› abbreviation small_steps ::
‹instruction × state ⇒ instruction × state ⇒ bool› (infix ‹→*› 55)
where ‹small_steps pre post ≡ (star small_step) pre post›
text ‹
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.
› schematic_goal ‹(x <- N 2 ;; y <- V x, λx.0) →* ?post› apply (rule star.trans) ― ‹force the execution of one step› apply (rule Seq) ― ‹apply the Seq rule to go to the first instruction› apply (rule Assign) ― ‹apply the Assign rule to handle it› apply simp ― ‹simplify to get the computed value of x› apply (rule star.trans) ― ‹go to the next step› apply (rule SeqNop) ― ‹get rid of the Nop we got when stepping through the assignment› apply (rule star.trans) ― ‹go to the next step› apply (rule Assign) ― ‹apply the Assign rule to handle it› apply simp ― ‹simplify to get the computed value of y› apply (rule star.refl) ― ‹apply the reflexivity rule to finish and get ?post› done text ‹so we can see that at the end, we have x and y = 2›
text ‹
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.
› values ‹{map (snd post) [x, y]
|post. (x<-(N 3);; y<-(V x), λx.0) →* post}›
text ‹
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)
›
text ‹
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 ∧ Q can be transformed into facts P and Q by eliminating ∧ (this is rule conjE). Since we defined → 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.
› text ‹Rule inversion› inductive_cases NopE[elim!]: ‹(Nop, pre) → cont› thm NopE inductive_cases VDeclE[elim!]: ‹(var x, s) → (i, s')› thm VDeclE inductive_cases AssignE[elim!]: ‹(x <- e, s) → (i, s')› thm AssignE inductive_cases SeqNopE[elim!]: ‹(Nop;; i2, s) → (i, s')› thm SeqNopE inductive_cases SeqE[elim!]: ‹(i1;; i2, pre) → cont› thm SeqE inductive_cases AltE[elim!]: ‹(if c then iT else iF fi, s) → (i, s')› thm AltE inductive_cases WhileE[elim]: ‹(while c do body done, s) → (i, s')› thm WhileE
text ‹
Prove that the small step semantics is deterministic: a given instruction executed in a given state always leads to the same state.
› theorem small_step_deterministic:
‹⟦pre → post; pre → post'⟧ ⟹ post' = post›
by (induction arbitrary: post' rule: small_step.induct, auto)
end (:endbrush:)