equal
deleted
inserted
replaced
54 |
54 |
55 abbreviation "w n == |
55 abbreviation "w n == |
56 WHILE Less (V ''y'') (N n) |
56 WHILE Less (V ''y'') (N n) |
57 DO ( ''y'' ::= Plus (V ''y'') (N 1); ''x'' ::= Plus (V ''x'') (V ''y'') )" |
57 DO ( ''y'' ::= Plus (V ''y'') (N 1); ''x'' ::= Plus (V ''x'') (V ''y'') )" |
58 |
58 |
59 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 \<le> n} ''x'' ::= N 0; ''y'' ::= N 0; w n {\<lambda>s. s ''x'' = \<Sum>{1..n}}" |
60 apply(rule Semi) |
60 apply(rule Semi) |
61 prefer 2 |
61 prefer 2 |
62 apply(rule While' |
62 apply(rule While' |
63 [where P = "\<lambda>s. s ''x'' = \<Sum> {1..s ''y''} \<and> 0 \<le> 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" |
64 and f = "\<lambda>s. nat (n - s ''y'')"]) |
64 and f = "\<lambda>s. nat (n - s ''y'')"]) |