97 {P1} A {Q1} {P2} B loops Q1 \<mapsto> P2 A well-formed |
97 {P1} A {Q1} {P2} B loops Q1 \<mapsto> P2 A well-formed |
98 ------------------------------------------------------ |
98 ------------------------------------------------------ |
99 {P1} A |+| B loops |
99 {P1} A |+| B loops |
100 *} |
100 *} |
101 |
101 |
|
102 |
|
103 |
|
104 |
102 lemma Hoare_plus_unhalt: |
105 lemma Hoare_plus_unhalt: |
103 assumes a_imp: "Q1 \<mapsto> P2" |
106 assumes a_imp: "Q1 \<mapsto> P2" |
104 and A_wf : "tm_wf (A, 0)" |
107 and A_wf : "tm_wf (A, 0)" |
105 and A_halt : "{P1} A {Q1}" |
108 and A_halt : "{P1} A {Q1}" |
106 and B_uhalt : "{P2} B \<up>" |
109 and B_uhalt : "{P2} B \<up>" |
125 then have "\<not> is_final (steps0 (Suc 0, l', r') B (n - n2))" by auto |
128 then have "\<not> is_final (steps0 (Suc 0, l', r') B (n - n2))" by auto |
126 then obtain s'' l'' r'' |
129 then obtain s'' l'' r'' |
127 where "steps0 (Suc 0, l', r') B (n - n2) = (s'', l'', r'')" |
130 where "steps0 (Suc 0, l', r') B (n - n2) = (s'', l'', r'')" |
128 and "\<not> is_final (s'', l'', r'')" by (metis surj_pair) |
131 and "\<not> is_final (s'', l'', r'')" by (metis surj_pair) |
129 then have "steps0 (Suc (length A div 2), l', r') (A |+| B) (n - n2) = (s''+ length A div 2, l'', r'')" |
132 then have "steps0 (Suc (length A div 2), l', r') (A |+| B) (n - n2) = (s''+ length A div 2, l'', r'')" |
130 using A_wf by (auto dest: t_merge_second_same simp del: steps.simps) |
133 using A_wf by (auto dest: t_merge_second_same simp del: tm_wf.simps) |
131 then have "\<not> is_final (steps0 (1, l, r) (A |+| B) (n2 + (n - n2)))" |
134 then have "\<not> is_final (steps0 (1, l, r) (A |+| B) (n2 + (n - n2)))" |
132 using A_wf by (simp only: steps_add eq) (simp add: tm_wf.simps) |
135 using A_wf by (simp only: steps_add eq) (simp add: tm_wf.simps) |
133 then show "\<not> is_final (steps0 (1, l, r) (A |+| B) n)" |
136 then show "\<not> is_final (steps0 (1, l, r) (A |+| B) n)" |
134 using `n2 \<le> n` by simp |
137 using `n2 \<le> n` by simp |
135 next |
138 next |
150 using assms |
153 using assms |
151 unfolding Hoare_def assert_imp_def |
154 unfolding Hoare_def assert_imp_def |
152 by (metis holds_for.simps surj_pair) |
155 by (metis holds_for.simps surj_pair) |
153 |
156 |
154 |
157 |
|
158 declare tm_comp.simps [simp del] |
|
159 declare adjust.simps[simp del] |
|
160 declare shift.simps[simp del] |
|
161 declare tm_wf.simps[simp del] |
155 declare step.simps[simp del] |
162 declare step.simps[simp del] |
156 declare steps.simps[simp del] |
163 declare steps.simps[simp del] |
157 declare tm_comp.simps [simp del] adjust.simps[simp del] shift.simps[simp del] |
|
158 declare tm_wf.simps[simp del] |
|
159 |
164 |
160 |
165 |
161 |
166 |
162 end |
167 end |