I agree 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.
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
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
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