equal
deleted
inserted
replaced
1 header{* Hoare Logic for Total Correctness *} |
1 header{* Hoare Logic for Total Correctness *} |
2 |
2 |
3 theory HoareT imports Hoare_Sound_Complete begin |
3 theory HoareT imports Hoare_Sound_Complete begin |
4 |
4 |
5 text{* |
5 text{* Note that this definition of total validity @{text"\<Turnstile>\<^sub>t"} only |
6 Now that we have termination, we can define |
6 works if execution is deterministic (which it is in our case). *} |
7 total validity, @{text"\<Turnstile>\<^sub>t"}, as partial validity and guaranteed termination:*} |
|
8 |
7 |
9 definition hoare_tvalid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" |
8 definition hoare_tvalid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" |
10 ("\<Turnstile>\<^sub>t {(1_)}/ (_)/ {(1_)}" 50) where |
9 ("\<Turnstile>\<^sub>t {(1_)}/ (_)/ {(1_)}" 50) where |
11 "\<Turnstile>\<^sub>t {P}c{Q} \<equiv> \<forall>s. P s \<longrightarrow> (\<exists>t. (c,s) \<Rightarrow> t \<and> Q t)" |
10 "\<Turnstile>\<^sub>t {P}c{Q} \<equiv> \<forall>s. P s \<longrightarrow> (\<exists>t. (c,s) \<Rightarrow> t \<and> Q t)" |
12 |
11 |
59 |
58 |
60 lemma "\<turnstile>\<^sub>t {\<lambda>s. 0 <= n} ''x'' ::= N 0; ''y'' ::= N 0; w n {\<lambda>s. s ''x'' = \<Sum> {1 .. n}}" |
59 lemma "\<turnstile>\<^sub>t {\<lambda>s. 0 <= n} ''x'' ::= N 0; ''y'' ::= N 0; w n {\<lambda>s. s ''x'' = \<Sum> {1 .. n}}" |
61 apply(rule Semi) |
60 apply(rule Semi) |
62 prefer 2 |
61 prefer 2 |
63 apply(rule While' |
62 apply(rule While' |
64 [where P = "\<lambda>s. s ''x'' = \<Sum> {1..s ''y''} \<and> 0 <= n \<and> 0 <= s ''y'' \<and> s ''y'' \<le> n" |
63 [where P = "\<lambda>s. s ''x'' = \<Sum> {1..s ''y''} \<and> 0 \<le> s ''y'' \<and> s ''y'' \<le> n" |
65 and f = "\<lambda>s. nat n - nat (s ''y'')"]) |
64 and f = "\<lambda>s. nat (n - s ''y'')"]) |
66 apply(rule Semi) |
65 apply(rule Semi) |
67 prefer 2 |
66 prefer 2 |
68 apply(rule Assign) |
67 apply(rule Assign) |
69 apply(rule Assign') |
68 apply(rule Assign') |
70 apply (simp add: atLeastAtMostPlus1_int_conv algebra_simps) |
69 apply (simp add: atLeastAtMostPlus1_int_conv algebra_simps) |
71 apply clarsimp |
70 apply clarsimp |
72 apply arith |
|
73 apply fastforce |
71 apply fastforce |
74 apply(rule Semi) |
72 apply(rule Semi) |
75 prefer 2 |
73 prefer 2 |
76 apply(rule Assign) |
74 apply(rule Assign) |
77 apply(rule Assign') |
75 apply(rule Assign') |