NikAxiomatic.thy

theory NikAxiomatic

imports NikBigStep NikDenotational

begin

text ‹
  Axiomatic semantics of Niklaus:
    define how instructions modify properties of the state of the execution machine
›

text ‹Type for an assertion on a state of the execution machine›
type_synonym assertion = "state ⇒ bool"

text ‹
  Definition of a valid Hoare pre/post assertion noted @{theory_text ‹⊨ {φ} P {ψ}›}
  Such a triplet is valid with regard to the operational semantics: if φ holds in
  some state s, if executing P in s leads to state t, then ψ holds in state t.
›
definition hoare_valid:: "assertion ⇒ instruction ⇒ assertion ⇒ bool" ("⊨ {_} _ {_}" 50)
where
  "⊨ {P} c {Q} = (∀s t. P s ∧ (c, s) ↝ t ⟶ Q t)"

text ‹
  We could also have defined the validity of Hoare triplets with regard 
  to the denotational semantics. This would be equivalent since we have shown that
  the denotational and operational semantics define the same relations between states.
›
definition hoare_valid_den:: "assertion ⇒ instruction ⇒ assertion ⇒ bool" ("⊨⇩d {_} _ {_}" 50)
where
  "⊨⇩d {P} c {Q} = (∀s t. P s ∧ (s, t) ∈ ⟦c⟧ ⟶ Q t)"

text ‹Substitution of an expression to a variable in a state›
abbreviation state_subst:: "expression ⇒ varname ⇒ state ⇒ state"
where "state_subst e v s ≡ s(v:= evaluate e s)"

text ‹
  Substitution of an expression to a variable in an assertion.
  This amounts to applying the assertion to a modified state where
  the expression has been substituted to the variable.
›
abbreviation assert_subst:: "assertion ⇒ expression ⇒ varname ⇒ assertion" ("_[with _ for _]" [1000,0,0] 999)
where
  "P[with e for x] ≡ P ∘ (state_subst e x)"

text ‹
  Semantic rules for the Hoare semantics of Niklaus.
  These rules are used to derive Hoare triples.
›
inductive hoare_sem:: "assertion ⇒ instruction ⇒ assertion ⇒ bool" ("⊢ {_} _ {_}" 50)
where
  Nop:   "⊢ {P} Nop {P}"
| VDecl: "⊢ {P[with (N 0) for v]} var v {P}"
| Assign:"⊢ {P[with u for v]} v <- u {P}"
| Seq:   "⟦ ⊢ {P} i1 {Q} ; ⊢ {Q} i2 {R} ⟧ ⟹ ⊢ {P} i1;; i2 {R}"
| If:    "⟦ ⊢ {λs. P s ∧ (evalbool c s)} iT {Q}; ⊢ {λs. P s ∧ ¬ (evalbool c s)} iF {Q} ⟧
          ⟹ ⊢ {P} if c then iT else iF fi {Q}"
| While: "⊢ {λs. P s ∧ evalbool c s} body {P} 
          ⟹ ⊢ {P} while c do body done {λs. P s ∧ ¬(evalbool c s)}"
| Conseq:"⟦∀s. P' s ⟶ P s; ⊢ {P} instr {Q}; ∀s. Q s ⟶ Q' s⟧ 
          ⟹ ⊢ {P'} instr {Q'}"

text ‹For proof automation, add these rules to simp and intro rules›
lemmas[simp, intro!] = Nop VDecl Assign Seq If

text ‹
  Generate elimination rules from the inductive predicate.
  These rules tell what we can derive from the different cases
  where the inductive predicate hoare_sem holds.
›
inductive_cases NopAxElim[elim!]:"⊢ {P} Nop {P}"
inductive_cases VDeclAxElim[elim!]:"⊢ {P[with (N 0) for v]} var v {P}"
inductive_cases AssignAxElim[elim!]:"⊢ {P[with u for v]} v <- u {P}"
inductive_cases SeqAxElim[elim!]:"⊢ {P} i1;; i2 {R}"
inductive_cases IfAxElim[elim!]:"⊢ {P} if c then iT else iF fi {Q}"
inductive_cases WhileAxElim[elim]:"⊢ {P} while c do body done {λs. P s ∧ ¬(evalbool c s)}"
inductive_cases ConseqAxElim[elim]:"⊢ {P'} instr {Q'}"

text ‹
  The following two lemmas are easier to use than Conseq
  1) We can always use a stronger precondition
›
lemma strengthen_pre:
  "⟦ ∀s. P' s ⟶ P s;  ⊢ {P} instr {Q} ⟧ ⟹ ⊢ {P'} instr {Q}"
by (rule Conseq, auto)

text ‹
  2) We can always get a weaker postcondition
›
lemma weaken_post:
  "⟦ ⊢ {P} instr {Q};  ∀s. Q s ⟶ Q' s ⟧ ⟹  ⊢ {P} instr {Q'}"
by (rule Conseq, auto)

text ‹Small example›
lemma "⊢ {λs. True} ''x'' <- N 2 {λs. s ''x'' = 2}"
apply (rule strengthen_pre[of "λs. True" "(λs. (s ''x'' = 2))[with N 2 for ''x'']"])
apply simp
apply (rule Assign)
done

text ‹
  Since this is still quite cumbersome, let's define an easier to use assignment rule
›
thm Assign
thm strengthen_pre
thm strengthen_pre[OF _ Assign]

lemma Assign': "∀s. P s ⟶ (Q[with u for v]) s ⟹ ⊢ {P} v <- u {Q}"
  apply (rule strengthen_pre[OF _ Assign])
  apply (simp)
done

text ‹Same example with the new Assignment rule›
lemma "⊢ {λs. True} ''x'' <- N 2 {λs. s ''x'' = 2}"
apply (rule Assign')
apply simp
done

text ‹Same thing for the While rule›
lemma While':
  assumes "⊢ {λs. P s ∧ evalbool c s} body {P}"
      and "∀s. P s ∧ ¬ evalbool c s ⟶ Q s"
    shows "⊢ {P} while c do body done {Q}"
thm assms
thm While
thm While[OF assms(1)]
thm weaken_post
thm weaken_post[OF While[OF assms(1)]]
thm weaken_post[OF While[OF assms(1)] assms(2)]
by(rule weaken_post[OF While[OF assms(1)] assms(2)])

end

NikAxWeakestPreconditionExercise.thy

theory NikAxWeakestPreconditionExercise

imports NikAxiomatic NikBigStepProperties

begin

text ‹
  We gave the rules to derive Hoare triplets: ⊢ {P} instr {Q}.
  Is this definition sound and complete?
    - soundness: if a Hoare triplet is derivable, it is valid?
    - completeness: if a Hoare triplet is valid, is it derivable?
›

text ‹Soundness : if a Hoare triplet is derivable, it is valid›
theorem axiomatic_sound:"⊢ {P} instr {Q} ⟹ ⊨ {P} instr {Q}"
proof(induction rule: hoare_sem.induct)
  case (Nop P)
  then show ?case sorry
next
  case (VDecl P v)
  then show ?case sorry
next
  case (Assign P u v)
  then show ?case sorry
next
  case (Seq P i1 Q i2 R)
  then show ?case sorry
next
  case (If P c iT Q iF)
then show ?case sorry
next
  case (While P c body) ― ‹This is the only difficult case›
  then show ?case sorry
next
  case (Conseq P' P instr Q Q')
  then show ?case sorry
qed
qed

text ‹
  Completeness : every valid Hoare triplet is derivable
  For this, we need to introduce the notion of weakest precondition.
  For a given instruction and postcondition, this is the precondition
  which makes the postcondition hold on any state that can be reached
  by executing the instruction.
›
text ‹
  Weakest precondition for validating postcondition Q after executing instruction instr
›
definition weakestpre :: "instruction ⇒ assertion ⇒ assertion"
where "weakestpre instr Q = (λs. undefined ― ‹FIXME›)"

text ‹Find the weakest precondition for each instruction›
lemma wp_Nop[simp]: "weakestpre Nop Q = undefined ― ‹FIXME›"
unfolding weakestpre_def sorry

lemma wp_Decl[simp]: "weakestpre (var x) Q = undefined ― ‹FIXME›"
unfolding weakestpre_def sorry

lemma wp_Assign[simp]: "weakestpre (x <- a) Q = undefined ― ‹FIXME›"
unfolding weakestpre_def sorry

lemma wp_Seq[simp]: "weakestpre (c⇩1;;c⇩2) Q = undefined ― ‹FIXME›"
unfolding weakestpre_def sorry

lemma wp_If[simp]:
 "weakestpre (if cond then iT else iF fi) Q =
 (λs. undefined ― ‹FIXME›)"
unfolding weakestpre_def sorry

text ‹Show that the weakest precondition does not change when unfolding a while loop›
lemma wp_While_unfold:
 "weakestpre (while cond do body done) Q s =
  weakestpre (Nop ― ‹FIXME›) Q s"
unfolding weakestpre_def
using unfold_while by auto

lemma wp_While_True[simp]:
  assumes ‹evalbool cond s›
  shows
     ‹weakestpre (while cond do body done) Q s
    = weakestpre (Nop ― ‹FIXME›) Q s›
using assms by(simp add: wp_While_unfold)

lemma wp_While_False[simp]:
  assumes ‹¬ evalbool cond s›
  shows
    ‹weakestpre (while cond do body done) Q s = undefined›
using assms sorry

text ‹Show that the weakest precondition is a valid precondition›
lemma weakestpre_is_pre: "⊢ {weakestpre instr Q} instr {Q}"
proof (induction instr arbitrary: Q)
  case Nop
  then show ?case sorry
next
  case (VarDecl x)
  then show ?case sorry
next
  case (Assign x1 x2a)
  then show ?case sorry
next
  case (Seq instr1 instr2)
  then show ?case sorry
next
  case (Alternative x1 instr1 instr2)
  then show ?case sorry
next
  case (While cond body)
  let ?w = "while cond do body done"
  show "⊢ {weakestpre ?w Q} ?w {Q}" sorry
qed

text ‹
  We can now show that the axiomatic semantics of Niklaus is complete with regard 
  to the validity of Hoare triplets (defined in terms of big step semantics)
›
theorem axiomatic_complete:
  assumes "⊨ {P} instr {Q}"
  shows   "⊢ {P} instr {Q}"
proof (rule strengthen_pre)
  show "∀s. P s ⟶P' s" sorry
  show "⊢ {P'} instr {Q}" sorry
qed

text ‹So the axiomatic semantics is sound and complete›
corollary axiomatic_sound_complete: "⊢ {P} instr {Q} ⟷ ⊨ {P} instr {Q}"
using axiomatic_sound and axiomatic_complete by auto

end

NiklausGCDExercise.thy

theory NiklausGCDExercise
imports NikAxiomatic

begin

text ‹
  We implement Euclid's subtraction algorithm in Niklaus and prove that it is correct.
›


section ‹Definition of the GCD›
― ‹You may use Isabelle's @term‹gcd a b› operator›
definition is_gcd :: ‹int ⇒ int ⇒ int ⇒ bool›
  where ‹is_gcd a b g ≡ undefined ― ‹FIX ME››

section ‹Other definitions and lemmas›

― ‹Hint: decompose the program into a if_then_else inside a loop, use abbreviations.›


section ‹Proof of the Niklaus implementation of  Euclid's algorithm›
― ‹Depending on your definition of is_gcd, you may have to use a stronger precondition›
lemma gcd_Euclid:
  ‹⊢ {λs. is_gcd (s ''x'') (s ''y'') k}
      while V ''x'' .≠. V ''y'' do
        if V ''x'' .<. V ''y'' then
          ''y'' <- V ''y'' .-. V ''x''
        else
          ''x'' <- V ''x'' .-. V ''y''
        fi
      done
     {λs. is_gcd (s ''x'') (s ''y'') (s ''x'')}›
sorry

― ‹Explain the meaning of the precondition and of the postcondition in plain language.›

end