174 apply(auto) |
174 apply(auto) |
175 done |
175 done |
176 |
176 |
177 type_synonym assert = "tape \<Rightarrow> bool" |
177 type_synonym assert = "tape \<Rightarrow> bool" |
178 |
178 |
179 definition assert_imp :: "assert \<Rightarrow> assert \<Rightarrow> bool" ("_ \<mapsto> _" [0, 0] 100) |
179 definition |
180 where |
180 assert_imp :: "assert \<Rightarrow> assert \<Rightarrow> bool" ("_ \<mapsto> _" [0, 0] 100) |
181 "assert_imp P Q = (\<forall>l r. P (l, r) \<longrightarrow> Q (l, r))" |
181 where |
|
182 "P \<mapsto> Q = (\<forall>l r. P (l, r) \<longrightarrow> Q (l, r))" |
182 |
183 |
183 lemma holds_for_imp: |
184 lemma holds_for_imp: |
184 assumes "P holds_for c" |
185 assumes "P holds_for c" |
185 and "P \<mapsto> Q" |
186 and "P \<mapsto> Q" |
186 shows "Q holds_for c" |
187 shows "Q holds_for c" |
187 using assms unfolding assert_imp_def by (case_tac c, auto) |
188 using assms unfolding assert_imp_def by (case_tac c, auto) |
188 |
189 |
189 lemma test: |
|
190 assumes "is_final (steps (1, (l, r)) p n1)" |
|
191 and "is_final (steps (1, (l, r)) p n2)" |
|
192 shows "Q holds_for (steps (1, (l, r)) p n1) \<longleftrightarrow> Q holds_for (steps (1, (l, r)) p n2)" |
|
193 proof - |
|
194 obtain n3 where "n1 = n2 + n3 \<or> n2 = n1 + n3" |
|
195 by (metis le_iff_add nat_le_linear) |
|
196 with assms show "Q holds_for (steps (1, (l, r)) p n1) \<longleftrightarrow> Q holds_for (steps (1, (l, r)) p n2)" |
|
197 by(case_tac p) (auto) |
|
198 qed |
|
199 |
|
200 definition |
190 definition |
201 Hoare :: "assert \<Rightarrow> tprog \<Rightarrow> assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" 50) |
191 Hoare :: "assert \<Rightarrow> tprog \<Rightarrow> assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" 50) |
202 where |
192 where |
203 "{P} p {Q} \<equiv> |
193 "{P} p {Q} \<equiv> |
204 (\<forall>l r. P (l, r) \<longrightarrow> (\<exists>n. is_final (steps (1, (l, r)) p n) \<and> Q holds_for (steps (1, (l, r)) p n)))" |
194 (\<forall>l r. P (l, r) \<longrightarrow> (\<exists>n. is_final (steps (1, (l, r)) p n) \<and> Q holds_for (steps (1, (l, r)) p n)))" |
502 = (0, l', r')" |
487 = (0, l', r')" |
503 using t_merge_second_same[where s = "0"] |
488 using t_merge_second_same[where s = "0"] |
504 apply(auto) |
489 apply(auto) |
505 done |
490 done |
506 |
491 |
|
492 |
|
493 text {* |
|
494 {P1} A {Q1} {P2} B {Q2} Q1 \<mapsto> P2 |
|
495 ----------------------------------- |
|
496 {P1} A |+| B {Q2} |
|
497 *} |
|
498 |
|
499 |
507 lemma Hoare_plus_halt: |
500 lemma Hoare_plus_halt: |
508 assumes aimpb: "Q1 \<mapsto> P2" |
501 assumes aimpb: "Q1 \<mapsto> P2" |
509 and A_wf : "tm_wf (A, 0)" |
502 and A_wf : "tm_wf (A, 0)" |
510 and B_wf : "tm_wf (B, 0)" |
503 and B_wf : "tm_wf (B, 0)" |
511 and A_halt : "{P1} (A, 0) {Q1}" |
504 and A_halt : "{P1} (A, 0) {Q1}" |
512 and B_halt : "{P2} (B, 0) {Q2}" |
505 and B_halt : "{P2} (B, 0) {Q2}" |
513 shows "{P1} (A |+| B, 0) {Q2}" |
506 shows "{P1} (A |+| B, 0) {Q2}" |
514 proof(rule HoareI) |
507 proof(rule HoareI) |
515 fix l r |
508 fix l r |
516 assume h: "P1 (l, r)" |
509 assume h: "P1 (l, r)" |
517 then obtain n1 where a: "is_final (steps (1, l, r) (A, 0) n1)" and b: "Q1 holds_for (steps (1, l, r) (A, 0) n1)" |
510 then obtain n1 |
|
511 where "is_final (steps (1, l, r) (A, 0) n1)" and "Q1 holds_for (steps (1, l, r) (A, 0) n1)" |
518 using A_halt unfolding Hoare_def by auto |
512 using A_halt unfolding Hoare_def by auto |
519 then obtain l' r' where "steps (1, l, r) (A, 0) n1 = (0, l', r')" and c: "Q1 holds_for (0, l', r')" |
513 then obtain l' r' where "steps (1, l, r) (A, 0) n1 = (0, l', r')" and c: "Q1 holds_for (0, l', r')" |
520 by(case_tac "steps (1, l, r) (A, 0) n1", auto) |
514 by(case_tac "steps (1, l, r) (A, 0) n1") (auto) |
521 then obtain stpa where d: "steps (1, l, r) (A |+| B, 0) stpa = (Suc (length A div 2), l', r')" |
515 then obtain stpa where d: "steps (1, l, r) (A |+| B, 0) stpa = (Suc (length A div 2), l', r')" |
522 using A_wf |
516 using A_wf by(rule_tac t_merge_pre_halt_same) (auto) |
523 by(rule_tac t_merge_pre_halt_same, auto) |
517 moreover |
524 from c aimpb have "P2 holds_for (0, l', r')" |
518 from c aimpb have "P2 holds_for (0, l', r')" |
525 by(rule holds_for_imp) |
519 by (rule holds_for_imp) |
526 from this have "P2 (l', r')" by auto |
520 then have "P2 (l', r')" by auto |
527 from this obtain n2 where e: "is_final (steps (1, l', r') (B, 0) n2)" and f: "Q2 holds_for (steps (1, l', r') (B, 0) n2)" |
521 then obtain n2 |
528 using B_halt unfolding Hoare_def |
522 where "is_final (steps (1, l', r') (B, 0) n2)" and "Q2 holds_for (steps (1, l', r') (B, 0) n2)" |
529 by auto |
523 using B_halt unfolding Hoare_def by auto |
530 then obtain l'' r'' where "steps (1, l', r') (B, 0) n2 = (0, l'', r'')" and g: "Q2 holds_for (0, l'', r'')" |
524 then obtain l'' r'' where "steps (1, l', r') (B, 0) n2 = (0, l'', r'')" and g: "Q2 holds_for (0, l'', r'')" |
531 by(case_tac "steps (1, l', r') (B, 0) n2", auto) |
525 by (case_tac "steps (1, l', r') (B, 0) n2", auto) |
532 from this have "steps (Suc (length A div 2), l', r') (A |+| B, 0) n2 |
526 then have "steps (Suc (length A div 2), l', r') (A |+| B, 0) n2 = (0, l'', r'')" |
533 = (0, l'', r'')" |
527 by (rule_tac t_merge_second_halt_same) (auto simp: A_wf B_wf) |
534 apply(rule_tac t_merge_second_halt_same, auto simp: A_wf B_wf) |
528 ultimately show |
535 done |
529 "\<exists>n. is_final (steps (1, l, r) (A |+| B, 0) n) \<and> Q2 holds_for (steps (1, l, r) (A |+| B, 0) n)" |
536 thus "\<exists>n. is_final (steps (1, l, r) (A |+| B, 0) n) \<and> Q2 holds_for (steps (1, l, r) (A |+| B, 0) n)" |
530 using g |
537 using d g |
|
538 apply(rule_tac x = "stpa + n2" in exI) |
531 apply(rule_tac x = "stpa + n2" in exI) |
539 apply(simp add: steps_add) |
532 apply(simp add: steps_add) |
540 done |
533 done |
541 qed |
534 qed |
542 |
535 |