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 Complex_Types |
66992
69673025292e
less global theories -- avoid confusion about special cases;
wenzelm
parents:
66453
diff
changeset
|
2 |
imports "HOL-SPARK.SPARK" |
45044 | 3 |
begin |
4 |
||
58310 | 5 |
datatype day = Mon | Tue | Wed | Thu | Fri | Sat | Sun |
45044 | 6 |
|
7 |
record two_fields = |
|
8 |
Field1 :: "int \<times> day \<Rightarrow> int" |
|
9 |
Field2 :: int |
|
10 |
||
11 |
spark_types |
|
12 |
complex_types__day = day |
|
13 |
complex_types__record_type = two_fields |
|
14 |
||
15 |
definition |
|
16 |
initialized3 :: "(int \<times> day \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool" where |
|
17 |
"initialized3 A i k = (\<forall>j\<in>{0..<k}. A (i, val j) = 0)" |
|
18 |
||
19 |
definition |
|
20 |
initialized2 :: "(int \<times> day \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> bool" where |
|
21 |
"initialized2 A i = (\<forall>j\<in>{0..<i}. initialized3 A j 7)" |
|
22 |
||
23 |
definition |
|
24 |
initialized :: "(int \<Rightarrow> two_fields) \<Rightarrow> int \<Rightarrow> bool" where |
|
25 |
"initialized A i = (\<forall>j\<in>{0..<i}. |
|
26 |
initialized2 (Field1 (A j)) 10 \<and> Field2 (A j) = 0)" |
|
27 |
||
28 |
spark_proof_functions |
|
29 |
complex_types__initialized = initialized |
|
30 |
complex_types__initialized2 = initialized2 |
|
31 |
complex_types__initialized3 = initialized3 |
|
32 |
||
33 |
(*<*) |
|
69605 | 34 |
spark_open \<open>complex_types_app/initialize\<close> |
45044 | 35 |
|
36 |
spark_vc procedure_initialize_1 |
|
37 |
by (simp add: initialized_def) |
|
38 |
||
39 |
spark_vc procedure_initialize_2 |
|
40 |
proof - |
|
41 |
from |
|
63167 | 42 |
\<open>initialized a loop__1__i\<close> |
43 |
\<open>initialized2 (Field1 (a loop__1__i)) 9\<close> |
|
44 |
\<open>initialized3 (Field1 (a loop__1__i)) 9 (pos Sun)\<close> |
|
45044 | 45 |
show ?C1 |
46 |
apply (auto simp add: initialized_def initialized2_def initialized3_def) |
|
47 |
apply (case_tac "j = 9") |
|
48 |
apply auto |
|
49 |
apply (case_tac "ja = 6") |
|
50 |
apply auto |
|
51 |
done |
|
52 |
from H5 |
|
53 |
show ?C2 by simp |
|
54 |
qed |
|
55 |
||
56 |
spark_vc procedure_initialize_3 |
|
57 |
by (simp add: initialized2_def) |
|
58 |
||
59 |
spark_vc procedure_initialize_4 |
|
60 |
proof - |
|
63167 | 61 |
from \<open>initialized a loop__1__i\<close> |
45044 | 62 |
show ?C1 by (simp add: initialized_def) |
63 |
from |
|
63167 | 64 |
\<open>initialized2 (Field1 (a loop__1__i)) loop__2__j\<close> |
65 |
\<open>initialized3 (Field1 (a loop__1__i)) loop__2__j (pos Sun)\<close> |
|
45044 | 66 |
show ?C2 |
67 |
apply (auto simp add: initialized2_def initialized3_def) |
|
68 |
apply (case_tac "j = loop__2__j") |
|
69 |
apply auto |
|
70 |
apply (case_tac "ja = 6") |
|
71 |
apply auto |
|
72 |
done |
|
73 |
from H5 |
|
74 |
show ?C3 by simp |
|
75 |
qed |
|
76 |
||
77 |
spark_vc procedure_initialize_5 |
|
78 |
by (simp add: initialized3_def) |
|
79 |
||
80 |
spark_vc procedure_initialize_6 |
|
81 |
proof - |
|
63167 | 82 |
from \<open>initialized a loop__1__i\<close> |
45044 | 83 |
show ?C1 by (simp add: initialized_def) |
63167 | 84 |
from \<open>initialized2 (Field1 (a loop__1__i)) loop__2__j\<close> |
45044 | 85 |
show ?C2 by (simp add: initialized2_def initialized3_def) |
86 |
from |
|
63167 | 87 |
\<open>initialized3 (Field1 (a loop__1__i)) loop__2__j (pos loop__3__k)\<close> |
88 |
\<open>loop__3__k < Sun\<close> |
|
45044 | 89 |
rangeI [of pos loop__3__k] |
90 |
show ?C3 |
|
91 |
apply (auto simp add: initialized3_def succ_def less_pos pos_val range_pos) |
|
92 |
apply (case_tac "j = pos loop__3__k") |
|
93 |
apply (auto simp add: val_pos) |
|
94 |
done |
|
95 |
from H5 |
|
96 |
show ?C4 by simp |
|
97 |
qed |
|
98 |
||
99 |
spark_vc procedure_initialize_9 |
|
100 |
using |
|
63167 | 101 |
\<open>initialized a 9\<close> |
102 |
\<open>initialized2 (Field1 (a 9)) 9\<close> |
|
103 |
\<open>initialized3 (Field1 (a 9)) 9 (pos Sun)\<close> |
|
45044 | 104 |
apply (auto simp add: initialized_def initialized2_def initialized3_def) |
105 |
apply (case_tac "j = 9") |
|
106 |
apply auto |
|
107 |
apply (case_tac "ja = 6") |
|
108 |
apply auto |
|
109 |
done |
|
110 |
||
111 |
spark_end |
|
112 |
(*>*) |
|
113 |
||
114 |
end |