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 (\<open>_ ::= _\<close> [1000, 61] 61)
| Seq com com (\<open>_;;/ _\<close> [60, 61] 60)
| If bexp com com (\<open>(IF _/ THEN _/ ELSE _)\<close> [0, 0, 61] 61)
| While bexp com (\<open>(WHILE _/ DO _)\<close> [0, 61] 61)
| Or com com (\<open>_ OR _\<close> [60, 60] 60)
| Assume bexp (\<open>ASSUME _\<close> [60] 60)
inductive big_step :: "com \<times> state \<Rightarrow> state \<Rightarrow> bool" (infix \<open>\<Rightarrow>\<close> 55)
where
Skip: "(SKIP,s) \<Rightarrow> s" |
Assign: "(x ::= a,s) \<Rightarrow> s(x := aval a s)" |
Seq: "\<lbrakk> (c\<^sub>1,s\<^sub>1) \<Rightarrow> s\<^sub>2; (c\<^sub>2,s\<^sub>2) \<Rightarrow> s\<^sub>3 \<rbrakk> \<Longrightarrow> (c\<^sub>1;;c\<^sub>2, s\<^sub>1) \<Rightarrow> s\<^sub>3" |
IfTrue: "\<lbrakk> bval b s; (c\<^sub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<Rightarrow> t" |
IfFalse: "\<lbrakk> \<not>bval b s; (c\<^sub>2,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<Rightarrow> t" |
WhileFalse: "\<not>bval b s \<Longrightarrow> (WHILE b DO c,s) \<Rightarrow> s" |
WhileTrue: "\<lbrakk> bval b s\<^sub>1; (c,s\<^sub>1) \<Rightarrow> s\<^sub>2; (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3 \<rbrakk> \<Longrightarrow> (WHILE b DO c, s\<^sub>1) \<Rightarrow> s\<^sub>3" |
Or_left: "(c1, s) \<Rightarrow> t \<Longrightarrow> (c1 OR c2, s) \<Rightarrow> t" |
Or_right: "(c2, s) \<Rightarrow> t \<Longrightarrow> (c1 OR c2, s) \<Rightarrow> t" |
Assume: "bval b s \<Longrightarrow> (ASSUME b, s) \<Rightarrow> s"
lemmas big_step_induct = big_step.induct[split_format(complete)]
declare big_step.intros[intro]
inductive_cases SkipE[elim!]: "(SKIP, s) \<Rightarrow> t"
inductive_cases AssignE[elim!]: "(x ::= a, s) \<Rightarrow> t"
inductive_cases SeqE[elim!]: "(c1;;c2,s1) \<Rightarrow> s3"
inductive_cases IfE[elim]: "(IF b THEN c1 ELSE c2,s) \<Rightarrow> t"
inductive_cases WhileE[elim]: "(WHILE b DO c,s) \<Rightarrow> t"
inductive_cases OrE[elim!]: "(c1 OR c2, s) \<Rightarrow> t"
inductive_cases AssumeE[elim!]: "(ASSUME b, s) \<Rightarrow> t"
abbreviation
equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" (infix \<open>\<sim>\<close> 50) where
"c \<sim> c' \<equiv> (\<forall>s t. (c,s) \<Rightarrow> t = (c',s) \<Rightarrow> t)"
lemma unfold_while:
"(WHILE b DO c) \<sim> (IF b THEN c;; WHILE b DO c ELSE SKIP)" (is "?w \<sim> ?iw")
proof -
\<comment> \<open>to show the equivalence, we look at the derivation tree for\<close>
\<comment> \<open>each side and from that construct a derivation tree for the other side\<close>
have "(?iw, s) \<Rightarrow> t" if assm: "(?w, s) \<Rightarrow> t" for s t
proof -
from assm show ?thesis
proof cases \<comment> \<open>rule inversion on \<open>(?w, s) \<Rightarrow> t\<close>\<close>
case WhileFalse
thus ?thesis by blast
next
case WhileTrue
from \<open>bval b s\<close> \<open>(?w, s) \<Rightarrow> t\<close> obtain s' where
"(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto
\<comment> \<open>now we can build a derivation tree for the \<^text>\<open>IF\<close>\<close>
\<comment> \<open>first, the body of the True-branch:\<close>
hence "(c;; ?w, s) \<Rightarrow> t" by (rule Seq)
\<comment> \<open>then the whole \<^text>\<open>IF\<close>\<close>
with \<open>bval b s\<close> show ?thesis by (rule IfTrue)
qed
qed
moreover
\<comment> \<open>now the other direction:\<close>
have "(?w, s) \<Rightarrow> t" if assm: "(?iw, s) \<Rightarrow> t" for s t
proof -
from assm show ?thesis
proof cases \<comment> \<open>rule inversion on \<open>(?iw, s) \<Rightarrow> t\<close>\<close>
case IfFalse
hence "s = t" by blast
thus ?thesis using \<open>\<not>bval b s\<close> by blast
next
case IfTrue
\<comment> \<open>and for this, only the Seq-rule is applicable:\<close>
from \<open>(c;; ?w, s) \<Rightarrow> t\<close> obtain s' where
"(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto
\<comment> \<open>with this information, we can build a derivation tree for \<^text>\<open>WHILE\<close>\<close>
with \<open>bval b s\<close> show ?thesis by (rule WhileTrue)
qed
qed
ultimately
show ?thesis by blast
qed
type_synonym assn = "state \<Rightarrow> bool"
definition
hoare_valid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" (\<open>\<Turnstile> {(1_)}/ (_)/ {(1_)}\<close> 50) where
"\<Turnstile> {P}c{Q} = (\<forall>s t. P s \<and> (c,s) \<Rightarrow> t \<longrightarrow> Q t)"
abbreviation state_subst :: "state \<Rightarrow> aexp \<Rightarrow> vname \<Rightarrow> state"
(\<open>_[_'/_]\<close> [1000,0,0] 999)
where "s[a/x] == s(x := aval a s)"
end
theory Submission
imports Defs
begin
section \<open>Hoare Logic\<close>
text \<open>
Consider the modification of IMP (@{typ com}) with nondeterministic choice "@{term "c\<^sub>1 OR c\<^sub>2"}" and the
assumption command "@{term "ASSUME b"}" as known from the tutorial, week 5; that is
"@{term "c\<^sub>1 OR c\<^sub>2"}" decides nondeterministically to execute \<open>c\<^sub>1\<close> or \<open>c\<^sub>2\<close>;
and "@{term "ASSUME b"}" behaves like "@{term SKIP}" if \<open>b\<close> evaluates to true and returns no result
otherwise.
First, complete the Hoare calculus rules for partial correctness of this language by providing the
missing rules for the new constructors. Do not modify the pre-defined rules!
\<close>
inductive
hoare :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" (\<open>\<turnstile> ({(1_)}/ (_)/ {(1_)})\<close> 50)
where
Skip: "\<turnstile> {P} SKIP {P}" |
Assign: "\<turnstile> {\<lambda>s. P(s[a/x])} x::=a {P}" |
Seq: "\<lbrakk> \<turnstile> {P} c\<^sub>1 {Q}; \<turnstile> {Q} c\<^sub>2 {R} \<rbrakk> \<Longrightarrow> \<turnstile> {P} c\<^sub>1;;c\<^sub>2 {R}" |
If: "\<lbrakk> \<turnstile> {\<lambda>s. P s \<and> bval b s} c\<^sub>1 {Q}; \<turnstile> {\<lambda>s. P s \<and> \<not> bval b s} c\<^sub>2 {Q} \<rbrakk>
\<Longrightarrow> \<turnstile> {P} IF b THEN c\<^sub>1 ELSE c\<^sub>2 {Q}" |
While: "\<turnstile> {\<lambda>s. P s \<and> bval b s} c {P} \<Longrightarrow>
\<turnstile> {P} WHILE b DO c {\<lambda>s. P s \<and> \<not> bval b s}" |
conseq: "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile> {P} c {Q}; \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk>
\<Longrightarrow> \<turnstile> {P'} c {Q'}" |
text \<open>
Here is just some setup. SCROLL TO THE NEXT EXERCISE BELOW!
\<close>
lemmas [simp] = hoare.Skip hoare.Assign hoare.Seq If
lemmas [intro!] = hoare.Skip hoare.Assign hoare.Seq hoare.If
lemma strengthen_pre:
"\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile> {P} c {Q} \<rbrakk> \<Longrightarrow> \<turnstile> {P'} c {Q}"
by (blast intro: conseq)
lemma weaken_post:
"\<lbrakk> \<turnstile> {P} c {Q}; \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk> \<Longrightarrow> \<turnstile> {P} c {Q'}"
by (blast intro: conseq)
lemma Assign': "\<forall>s. P s \<longrightarrow> Q(s[a/x]) \<Longrightarrow> \<turnstile> {P} x ::= a {Q}"
by (simp add: strengthen_pre[OF _ Assign])
lemma While':
assumes "\<turnstile> {\<lambda>s. P s \<and> bval b s} c {P}" and "\<forall>s. P s \<and> \<not> bval b s \<longrightarrow> Q s"
shows "\<turnstile> {P} WHILE b DO c {Q}"
by(rule weaken_post[OF While[OF assms(1)] assms(2)])
lemma hoare_sound: "\<turnstile> {P}c{Q} \<Longrightarrow> \<Turnstile> {P}c{Q}"
proof(induction rule: hoare.induct)
case (While P b c)
have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> P s \<Longrightarrow> P t \<and> \<not> bval b t" for s t
proof(induction "WHILE b DO c" s t rule: big_step_induct)
case WhileFalse thus ?case by blast
next
case WhileTrue thus ?case
using While.IH unfolding hoare_valid_def by blast
qed
thus ?case unfolding hoare_valid_def by blast
qed (auto simp: hoare_valid_def)
definition wp :: "com \<Rightarrow> assn \<Rightarrow> assn" where
"wp c Q = (\<lambda>s. \<forall>t. (c,s) \<Rightarrow> t \<longrightarrow> Q t)"
lemma wp_SKIP[simp]: "wp SKIP Q = Q"
by (rule ext) (auto simp: wp_def)
lemma wp_Ass[simp]: "wp (x::=a) Q = (\<lambda>s. Q(s[a/x]))"
by (rule ext) (auto simp: wp_def)
lemma wp_Seq[simp]: "wp (c\<^sub>1;;c\<^sub>2) Q = wp c\<^sub>1 (wp c\<^sub>2 Q)"
by (rule ext) (auto simp: wp_def)
lemma wp_If[simp]:
"wp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) Q =
(\<lambda>s. if bval b s then wp c\<^sub>1 Q s else wp c\<^sub>2 Q s)"
by (rule ext) (auto simp: wp_def)
lemma wp_While_If:
"wp (WHILE b DO c) Q s =
wp (IF b THEN c;;WHILE b DO c ELSE SKIP) Q s"
unfolding wp_def by (metis unfold_while)
lemma wp_While_True[simp]: "bval b s \<Longrightarrow>
wp (WHILE b DO c) Q s = wp (c;; WHILE b DO c) Q s"
by(simp add: wp_While_If)
lemma wp_While_False[simp]: "\<not> bval b s \<Longrightarrow> wp (WHILE b DO c) Q s = Q s"
by(simp add: wp_While_If)
text \<open>
Next give appropriate, simple definitions \<open>wp_Or\<close> and \<open>wp_Assume\<close> for the weakest preconditions of
"@{term "c1 OR c2"}" and "@{term "ASSUME b"}", respectively.
The definition must subject to the following conditions:
\<^item> It holds that "\<open>wp (c1 OR c2) Q = wp_Or c1 c2 Q\<close>" and "\<open>wp (ASSUME b) Q = wp_Assume b Q\<close>".
\<^item> The rules must be simple and not merely be a restatement of the definition of @{term wp}. In
particular, your definitions may not use quantifiers (forall, exists).
\<^item> The definition of "\<open>wp_Or c1 c2 Q\<close>" for "@{term "c1 OR c2"}" must use
"@{term "wp c1 Q"}" as well as "@{term "wp c2 Q"}".
\<close>
(*must use "wp c1 Q" as well as "wp c2 q"*)
definition wp_Or :: "com \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> assn" where
"wp_Or \<equiv> undefined"
definition wp_Assume :: "bexp \<Rightarrow> assn \<Rightarrow> assn" where
"wp_Assume \<equiv> undefined"
text \<open>
Finally show that your Hoare rules are sound and complete by filling out the missing proof steps
below.
\<close>
lemma wp_is_pre: "\<turnstile> {wp c Q} c {Q}"
proof(induction c arbitrary: Q)
case If thus ?case by(auto intro: conseq)
next
case (While b c)
let ?w = "WHILE b DO c"
show "\<turnstile> {wp ?w Q} ?w {Q}"
proof(rule While')
show "\<turnstile> {\<lambda>s. wp ?w Q s \<and> bval b s} c {wp ?w Q}"
proof(rule strengthen_pre[OF _ While.IH])
show "\<forall>s. wp ?w Q s \<and> bval b s \<longrightarrow> wp c (wp ?w Q) s" by auto
qed
show "\<forall>s. wp ?w Q s \<and> \<not> bval b s \<longrightarrow> Q s" by auto
qed
next
case (Assume x)
then show ?case sorry
next
case (Or c1 c2)
then show ?case sorry
qed auto
lemma hoare_complete: assumes "\<Turnstile> {P}c{Q}" shows "\<turnstile> {P}c{Q}"
proof(rule strengthen_pre)
show "\<forall>s. P s \<longrightarrow> wp c Q s" using assms
by (auto simp: hoare_valid_def wp_def)
show "\<turnstile> {wp c Q} c {Q}" by(rule wp_is_pre)
qed
corollary hoare_sound_complete: "\<turnstile> {P}c{Q} \<longleftrightarrow> \<Turnstile> {P}c{Q}"
by (metis hoare_complete hoare_sound)
end
theory Check imports Submission begin end