Homework 09.1

Definitions File

theory Defs
 imports "HOL-IMP.BExp"
begin

datatype
com = SKIP
    | Assign vname aexp       ("_ ::= _" [1000, 61] 61)
    | Seq    com  com         ("_;;/ _"  [60, 61] 60)
    | If     bexp com com     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61)
    | While  bexp com         ("(WHILE _/ DO _)"  [0, 61] 61)
    | CONTINUE

inductive
  big_step :: "com × state ⇒ bool × state ⇒ bool" (infix "⇒" 55)
where
Skip: "(SKIP,s) ⇒ (False,s)" |
Assign: "(x ::= a,s) ⇒ (False,s(x := aval a s))" |
Seq1: "⟦ (c⇩1,s⇩1) ⇒ (False,s⇩2);  (c⇩2,s⇩2) ⇒ s⇩3 ⟧ ⟹ (c⇩1;;c⇩2, s⇩1) ⇒ s⇩3" |
Seq2: "⟦ (c⇩1,s⇩1) ⇒ (True,s⇩2) ⟧ ⟹ (c⇩1;;c⇩2, s⇩1) ⇒ (True,s⇩2)" |
IfTrue: "⟦ bval b s;  (c⇩1,s) ⇒ t ⟧ ⟹ (IF b THEN c⇩1 ELSE c⇩2, s) ⇒ t" |
IfFalse: "⟦ ¬bval b s;  (c⇩2,s) ⇒ t ⟧ ⟹ (IF b THEN c⇩1 ELSE c⇩2, s) ⇒ t" |
WhileFalse: "¬bval b s ⟹ (WHILE b DO c,s) ⇒ (False,s)" |
WhileTrue:
"⟦ bval b s⇩1;  (c,s⇩1) ⇒ (_, s⇩2);  (WHILE b DO c, s⇩2) ⇒ s⇩3 ⟧
⟹ (WHILE b DO c, s⇩1) ⇒ s⇩3" | ― ‹We can simply reset the continue flag in a while loop›
Continue: "(CONTINUE,s) ⇒ (True,s)"

text‹Proof automation:›

text ‹The introduction rules are good for automatically
constructing small program executions. The recursive cases
may require backtracking, so we declare the set as unsafe
intro rules.›
declare big_step.intros [intro]

text‹The standard induction rule
@{thm [display] big_step.induct [no_vars]}›

thm big_step.induct

text‹
This induction schema is almost perfect for our purposes, but
our trick for reusing the tuple syntax means that the induction
schema has two parameters instead of the ‹c›, ‹s›,
and ‹s'› that we are likely to encounter. Splitting
the tuple parameter fixes this:
›
lemmas big_step_induct = big_step.induct[split_format(complete)]
thm big_step_induct
text ‹
@{thm [display] big_step_induct [no_vars]}
›

text‹What can we deduce from @{prop "(SKIP,s) ⇒ t"} ?
That @{prop "s = t"}. This is how we can automatically prove it:›

inductive_cases SkipE[elim!]: "(SKIP,s) ⇒ t"
thm SkipE

inductive_cases ContinueE[elim!]: "(CONTINUE,s) ⇒ t"

text‹This is an \emph{elimination rule}. The [elim] attribute tells auto,
blast and friends (but not simp!) to use it automatically; [elim!] means that
it is applied eagerly.

Similarly for the other commands:›

inductive_cases AssignE[elim!]: "(x ::= a,s) ⇒ t"
thm AssignE
inductive_cases SeqE[elim!]: "(c1;;c2,s1) ⇒ s3"
thm SeqE
inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) ⇒ t"
thm IfE

inductive_cases WhileE[elim]: "(WHILE b DO c,s) ⇒ t"
thm WhileE
text‹Only [elim]: [elim!] would not terminate.›

abbreviation state_subst :: "state ⇒ aexp ⇒ vname ⇒ state"
  ("_[_'/_]" [1000,0,0] 999)
where "s[a/x] == s(x := aval a s)"

type_synonym assn = "state ⇒ bool"

definition
hoare_valid :: "assn ⇒ com ⇒ assn ⇒ bool" ("⊨ {(1_)}/ (_)/ {(1_)}" 50) where
  "⊨ {P}c{Q} = (∀s f t. P s ∧ (c,s) ⇒ (f, t)  ⟶  Q t)"

definition
hoare_valid⇩c :: "assn ⇒ assn ⇒ com ⇒ assn ⇒ bool" ("⊨⇩c{(1_)}/ {(1_)}/ (_)/ {(1_)}" 50) where
  "⊨⇩c{I} {P}c{Q} = (∀s f t. P s ∧ (c,s) ⇒ (f, t)  ⟶ (if f then I t else Q t))"

end

Template File

theory Submission
  imports Defs
begin

inductive
  hoare :: "assn ⇒ assn ⇒ com ⇒ assn ⇒ bool" ("⊢{(1_)}/ ({(1_)}/ (_)/ {(1_)})" 50)
where
Skip: "⊢{I} {P} SKIP {P}"  |
Assign:  "⊢{I} {λs. P(s[a/x])} x::=a {P}"  |
Seq: "⟦ ⊢{I} {P} c⇩1 {Q};  ⊢{I} {Q} c⇩2 {R} ⟧
      ⟹ ⊢{I} {P} c⇩1;;c⇩2 {R}"  |
If: "⟦ ⊢{I} {λs. P s ∧ bval b s} c⇩1 {Q};  ⊢{I} {λs. P s ∧ ¬ bval b s} c⇩2 {Q} ⟧
     ⟹ ⊢{I} {P} IF b THEN c⇩1 ELSE c⇩2 {Q}"  |
conseq: "⟦ ∀s. P' s ⟶ P s;  ⊢{I} {P} c {Q};  ∀s. Q s ⟶ Q' s ⟧
        ⟹ ⊢{I} {P'} c {Q'}"
― ‹Your cases here:›

theorem hoare_sound: "⊢{I} {P}c{Q} ⟹ ⊨⇩c{I} {P}c{Q}"
  sorry

definition wp :: "com ⇒ assn ⇒ assn ⇒ assn" where
  "wp c I Q = undefined"

theorem wp_is_pre: "⊢{I} {wp c I Q} c {Q}"
  sorry

theorem hoare_sound_complete: "⊢{Q} {P}c{Q} ⟷ ⊨ {P}c{Q}"
  sorry

end

Check File

theory Check
  imports Submission
begin

theorem hoare_sound: "⊢{I} {P}c{Q} ⟹ ⊨⇩c{I} {P}c{Q}"
  by (rule Submission.hoare_sound)

theorem wp_is_pre: "⊢{I} {wp c I Q} c {Q}"
  by (rule Submission.wp_is_pre)

theorem hoare_sound_complete: "⊢{Q} {P}c{Q} ⟷ ⊨ {P}c{Q}"
  by (rule Submission.hoare_sound_complete)

end