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:)

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:)

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:)

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:)

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:)