| author | paulson <lp15@cam.ac.uk> |
| Mon, 13 May 2024 22:42:40 +0100 | |
| changeset 80177 | 1478555580af |
| parent 69605 | a96320074298 |
| permissions | -rw-r--r-- |
| 45044 | 1 |
theory Proc1 |
|
66992
69673025292e
less global theories -- avoid confusion about special cases;
wenzelm
parents:
66453
diff
changeset
|
2 |
imports "HOL-SPARK.SPARK" |
| 45044 | 3 |
begin |
4 |
||
| 69605 | 5 |
spark_open \<open>loop_invariant/proc1\<close> |
| 45044 | 6 |
|
7 |
spark_vc procedure_proc1_5 |
|
|
64593
50c715579715
reoriented congruence rules in non-explosive direction
haftmann
parents:
58130
diff
changeset
|
8 |
by (simp add: ring_distribs mod_simps) |
| 45044 | 9 |
|
10 |
spark_vc procedure_proc1_8 |
|
|
64593
50c715579715
reoriented congruence rules in non-explosive direction
haftmann
parents:
58130
diff
changeset
|
11 |
by (simp add: ring_distribs mod_simps) |
| 45044 | 12 |
|
13 |
spark_end |
|
14 |
||
15 |
lemma pow_2_32_simp: "4294967296 = (2::int)^32" |
|
16 |
by simp |
|
17 |
||
18 |
end |