author | wenzelm |
Tue, 03 Sep 2013 01:12:40 +0200 | |
changeset 53374 | a14d2a854c02 |
parent 45044 | 2fae15f8984d |
child 56798 | 939e88e79724 |
permissions | -rw-r--r-- |
45044 | 1 |
theory Proc1 |
2 |
imports SPARK |
|
3 |
begin |
|
4 |
||
5 |
spark_open "loop_invariant/proc1.siv" |
|
6 |
||
7 |
spark_vc procedure_proc1_5 |
|
8 |
by (simp add: ring_distribs pull_mods) |
|
9 |
||
10 |
spark_vc procedure_proc1_8 |
|
11 |
by (simp add: ring_distribs pull_mods) |
|
12 |
||
13 |
spark_end |
|
14 |
||
15 |
lemma pow_2_32_simp: "4294967296 = (2::int)^32" |
|
16 |
by simp |
|
17 |
||
18 |
end |