equal
deleted
inserted
replaced
49 |
49 |
50 text{* Note that we deal with sequences of commands from right to left, |
50 text{* Note that we deal with sequences of commands from right to left, |
51 pulling back the postcondition towards the precondition. *} |
51 pulling back the postcondition towards the precondition. *} |
52 |
52 |
53 lemma "\<turnstile> {\<lambda>s. 0 <= n} ''x'' ::= N 0; ''y'' ::= N 0; w n {\<lambda>s. s ''x'' = \<Sum> {1 .. n}}" |
53 lemma "\<turnstile> {\<lambda>s. 0 <= n} ''x'' ::= N 0; ''y'' ::= N 0; w n {\<lambda>s. s ''x'' = \<Sum> {1 .. n}}" |
54 apply(rule hoare.Semi) |
54 apply(rule hoare.Seq) |
55 prefer 2 |
55 prefer 2 |
56 apply(rule While' |
56 apply(rule While' |
57 [where P = "\<lambda>s. s ''x'' = \<Sum> {1..s ''y''} \<and> 0 \<le> s ''y'' \<and> s ''y'' \<le> n"]) |
57 [where P = "\<lambda>s. s ''x'' = \<Sum> {1..s ''y''} \<and> 0 \<le> s ''y'' \<and> s ''y'' \<le> n"]) |
58 apply(rule Semi) |
58 apply(rule Seq) |
59 prefer 2 |
59 prefer 2 |
60 apply(rule Assign) |
60 apply(rule Assign) |
61 apply(rule Assign') |
61 apply(rule Assign') |
62 apply(fastforce simp: atLeastAtMostPlus1_int_conv algebra_simps) |
62 apply(fastforce simp: atLeastAtMostPlus1_int_conv algebra_simps) |
63 apply(fastforce) |
63 apply(fastforce) |
64 apply(rule Semi) |
64 apply(rule Seq) |
65 prefer 2 |
65 prefer 2 |
66 apply(rule Assign) |
66 apply(rule Assign) |
67 apply(rule Assign') |
67 apply(rule Assign') |
68 apply simp |
68 apply simp |
69 done |
69 done |