equal
deleted
inserted
replaced
37 by (simp add: initialized_def) |
37 by (simp add: initialized_def) |
38 |
38 |
39 spark_vc procedure_initialize_2 |
39 spark_vc procedure_initialize_2 |
40 proof - |
40 proof - |
41 from |
41 from |
42 `initialized a loop__1__i` |
42 \<open>initialized a loop__1__i\<close> |
43 `initialized2 (Field1 (a loop__1__i)) 9` |
43 \<open>initialized2 (Field1 (a loop__1__i)) 9\<close> |
44 `initialized3 (Field1 (a loop__1__i)) 9 (pos Sun)` |
44 \<open>initialized3 (Field1 (a loop__1__i)) 9 (pos Sun)\<close> |
45 show ?C1 |
45 show ?C1 |
46 apply (auto simp add: initialized_def initialized2_def initialized3_def) |
46 apply (auto simp add: initialized_def initialized2_def initialized3_def) |
47 apply (case_tac "j = 9") |
47 apply (case_tac "j = 9") |
48 apply auto |
48 apply auto |
49 apply (case_tac "ja = 6") |
49 apply (case_tac "ja = 6") |
56 spark_vc procedure_initialize_3 |
56 spark_vc procedure_initialize_3 |
57 by (simp add: initialized2_def) |
57 by (simp add: initialized2_def) |
58 |
58 |
59 spark_vc procedure_initialize_4 |
59 spark_vc procedure_initialize_4 |
60 proof - |
60 proof - |
61 from `initialized a loop__1__i` |
61 from \<open>initialized a loop__1__i\<close> |
62 show ?C1 by (simp add: initialized_def) |
62 show ?C1 by (simp add: initialized_def) |
63 from |
63 from |
64 `initialized2 (Field1 (a loop__1__i)) loop__2__j` |
64 \<open>initialized2 (Field1 (a loop__1__i)) loop__2__j\<close> |
65 `initialized3 (Field1 (a loop__1__i)) loop__2__j (pos Sun)` |
65 \<open>initialized3 (Field1 (a loop__1__i)) loop__2__j (pos Sun)\<close> |
66 show ?C2 |
66 show ?C2 |
67 apply (auto simp add: initialized2_def initialized3_def) |
67 apply (auto simp add: initialized2_def initialized3_def) |
68 apply (case_tac "j = loop__2__j") |
68 apply (case_tac "j = loop__2__j") |
69 apply auto |
69 apply auto |
70 apply (case_tac "ja = 6") |
70 apply (case_tac "ja = 6") |
77 spark_vc procedure_initialize_5 |
77 spark_vc procedure_initialize_5 |
78 by (simp add: initialized3_def) |
78 by (simp add: initialized3_def) |
79 |
79 |
80 spark_vc procedure_initialize_6 |
80 spark_vc procedure_initialize_6 |
81 proof - |
81 proof - |
82 from `initialized a loop__1__i` |
82 from \<open>initialized a loop__1__i\<close> |
83 show ?C1 by (simp add: initialized_def) |
83 show ?C1 by (simp add: initialized_def) |
84 from `initialized2 (Field1 (a loop__1__i)) loop__2__j` |
84 from \<open>initialized2 (Field1 (a loop__1__i)) loop__2__j\<close> |
85 show ?C2 by (simp add: initialized2_def initialized3_def) |
85 show ?C2 by (simp add: initialized2_def initialized3_def) |
86 from |
86 from |
87 `initialized3 (Field1 (a loop__1__i)) loop__2__j (pos loop__3__k)` |
87 \<open>initialized3 (Field1 (a loop__1__i)) loop__2__j (pos loop__3__k)\<close> |
88 `loop__3__k < Sun` |
88 \<open>loop__3__k < Sun\<close> |
89 rangeI [of pos loop__3__k] |
89 rangeI [of pos loop__3__k] |
90 show ?C3 |
90 show ?C3 |
91 apply (auto simp add: initialized3_def succ_def less_pos pos_val range_pos) |
91 apply (auto simp add: initialized3_def succ_def less_pos pos_val range_pos) |
92 apply (case_tac "j = pos loop__3__k") |
92 apply (case_tac "j = pos loop__3__k") |
93 apply (auto simp add: val_pos) |
93 apply (auto simp add: val_pos) |
96 show ?C4 by simp |
96 show ?C4 by simp |
97 qed |
97 qed |
98 |
98 |
99 spark_vc procedure_initialize_9 |
99 spark_vc procedure_initialize_9 |
100 using |
100 using |
101 `initialized a 9` |
101 \<open>initialized a 9\<close> |
102 `initialized2 (Field1 (a 9)) 9` |
102 \<open>initialized2 (Field1 (a 9)) 9\<close> |
103 `initialized3 (Field1 (a 9)) 9 (pos Sun)` |
103 \<open>initialized3 (Field1 (a 9)) 9 (pos Sun)\<close> |
104 apply (auto simp add: initialized_def initialized2_def initialized3_def) |
104 apply (auto simp add: initialized_def initialized2_def initialized3_def) |
105 apply (case_tac "j = 9") |
105 apply (case_tac "j = 9") |
106 apply auto |
106 apply auto |
107 apply (case_tac "ja = 6") |
107 apply (case_tac "ja = 6") |
108 apply auto |
108 apply auto |