###### Cookies disclaimer

Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

# Homework 09.1

This is the task corresponding to the first part of homework 9.

## Resources

Download Files

### 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

Terms and Conditions