equal
deleted
inserted
replaced
1 (* Author: Tobias Nipkow *) |
1 (* Author: Tobias Nipkow *) |
2 |
2 |
3 theory Hoare_Sound_Complete imports Hoare begin |
3 theory Hoare_Sound_Complete imports Hoare begin |
4 |
4 |
5 subsection "Soundness" |
5 subsection "Soundness" |
6 |
|
7 definition |
|
8 hoare_valid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<Turnstile> {(1_)}/ (_)/ {(1_)}" 50) where |
|
9 "\<Turnstile> {P}c{Q} = (\<forall>s t. (c,s) \<Rightarrow> t \<longrightarrow> P s \<longrightarrow> Q t)" |
|
10 |
6 |
11 lemma hoare_sound: "\<turnstile> {P}c{Q} \<Longrightarrow> \<Turnstile> {P}c{Q}" |
7 lemma hoare_sound: "\<turnstile> {P}c{Q} \<Longrightarrow> \<Turnstile> {P}c{Q}" |
12 proof(induction rule: hoare.induct) |
8 proof(induction rule: hoare.induct) |
13 case (While P b c) |
9 case (While P b c) |
14 { fix s t |
10 { fix s t |