equal
deleted
inserted
replaced
1 (* Author: Tobias Nipkow *) |
1 (* Author: Tobias Nipkow *) |
2 |
2 |
3 theory Hoare_Sound_Complete imports Hoare begin |
3 subsection \<open>Soundness and Completeness\<close> |
4 |
4 |
5 subsection "Soundness" |
5 theory Hoare_Sound_Complete |
|
6 imports Hoare |
|
7 begin |
|
8 |
|
9 subsubsection "Soundness" |
6 |
10 |
7 lemma hoare_sound: "\<turnstile> {P}c{Q} \<Longrightarrow> \<Turnstile> {P}c{Q}" |
11 lemma hoare_sound: "\<turnstile> {P}c{Q} \<Longrightarrow> \<Turnstile> {P}c{Q}" |
8 proof(induction rule: hoare.induct) |
12 proof(induction rule: hoare.induct) |
9 case (While P b c) |
13 case (While P b c) |
10 { fix s t |
14 { fix s t |
18 } |
22 } |
19 thus ?case unfolding hoare_valid_def by blast |
23 thus ?case unfolding hoare_valid_def by blast |
20 qed (auto simp: hoare_valid_def) |
24 qed (auto simp: hoare_valid_def) |
21 |
25 |
22 |
26 |
23 subsection "Weakest Precondition" |
27 subsubsection "Weakest Precondition" |
24 |
28 |
25 definition wp :: "com \<Rightarrow> assn \<Rightarrow> assn" where |
29 definition wp :: "com \<Rightarrow> assn \<Rightarrow> assn" where |
26 "wp c Q = (\<lambda>s. \<forall>t. (c,s) \<Rightarrow> t \<longrightarrow> Q t)" |
30 "wp c Q = (\<lambda>s. \<forall>t. (c,s) \<Rightarrow> t \<longrightarrow> Q t)" |
27 |
31 |
28 lemma wp_SKIP[simp]: "wp SKIP Q = Q" |
32 lemma wp_SKIP[simp]: "wp SKIP Q = Q" |
50 |
54 |
51 lemma wp_While_False[simp]: "\<not> bval b s \<Longrightarrow> wp (WHILE b DO c) Q s = Q s" |
55 lemma wp_While_False[simp]: "\<not> bval b s \<Longrightarrow> wp (WHILE b DO c) Q s = Q s" |
52 by(simp add: wp_While_If) |
56 by(simp add: wp_While_If) |
53 |
57 |
54 |
58 |
55 subsection "Completeness" |
59 subsubsection "Completeness" |
56 |
60 |
57 lemma wp_is_pre: "\<turnstile> {wp c Q} c {Q}" |
61 lemma wp_is_pre: "\<turnstile> {wp c Q} c {Q}" |
58 proof(induction c arbitrary: Q) |
62 proof(induction c arbitrary: Q) |
59 case If thus ?case by(auto intro: conseq) |
63 case If thus ?case by(auto intro: conseq) |
60 next |
64 next |