author | blanchet |
Mon, 01 Sep 2014 18:42:02 +0200 | |
changeset 58130 | 5e9170812356 |
parent 56798 | 939e88e79724 |
child 58310 | 91ea607a34d8 |
permissions | -rw-r--r-- |
45044 | 1 |
theory Complex_Types |
58130 | 2 |
imports "../SPARK" |
45044 | 3 |
begin |
4 |
||
58130 | 5 |
datatype_new 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 |
(*<*) |
|
56798
939e88e79724
Discontinued old spark_open; spark_open_siv is now spark_open
berghofe
parents:
45044
diff
changeset
|
34 |
spark_open "complex_types_app/initialize" |
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 |
|
42 |
`initialized a loop__1__i` |
|
43 |
`initialized2 (Field1 (a loop__1__i)) 9` |
|
44 |
`initialized3 (Field1 (a loop__1__i)) 9 (pos Sun)` |
|
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 - |
|
61 |
from `initialized a loop__1__i` |
|
62 |
show ?C1 by (simp add: initialized_def) |
|
63 |
from |
|
64 |
`initialized2 (Field1 (a loop__1__i)) loop__2__j` |
|
65 |
`initialized3 (Field1 (a loop__1__i)) loop__2__j (pos Sun)` |
|
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 - |
|
82 |
from `initialized a loop__1__i` |
|
83 |
show ?C1 by (simp add: initialized_def) |
|
84 |
from `initialized2 (Field1 (a loop__1__i)) loop__2__j` |
|
85 |
show ?C2 by (simp add: initialized2_def initialized3_def) |
|
86 |
from |
|
87 |
`initialized3 (Field1 (a loop__1__i)) loop__2__j (pos loop__3__k)` |
|
88 |
`loop__3__k < Sun` |
|
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 |
|
101 |
`initialized a 9` |
|
102 |
`initialized2 (Field1 (a 9)) 9` |
|
103 |
`initialized3 (Field1 (a 9)) 9 (pos Sun)` |
|
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 |