NikOpNaiveExercise.thy

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

NikBigStepExercise.thy

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

NikBigStepProperties.thy

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

NikSmallStep.thy

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