145 fun |
145 fun |
146 tm_comp :: "instr list \<Rightarrow> instr list \<Rightarrow> instr list" ("_ |+| _" [0, 0] 100) |
146 tm_comp :: "instr list \<Rightarrow> instr list \<Rightarrow> instr list" ("_ |+| _" [0, 0] 100) |
147 where |
147 where |
148 "tm_comp p1 p2 = ((adjust p1) @ (shift p2 (length p1 div 2)))" |
148 "tm_comp p1 p2 = ((adjust p1) @ (shift p2 (length p1 div 2)))" |
149 |
149 |
|
150 lemma step_0 [simp]: |
|
151 shows "step (0, (l, r)) p = (0, (l, r))" |
|
152 by (case_tac p, simp) |
|
153 |
|
154 lemma steps_0 [simp]: |
|
155 shows "steps (0, (l, r)) p n = (0, (l, r))" |
|
156 by (induct n) (simp_all) |
|
157 |
150 fun |
158 fun |
151 is_final :: "config \<Rightarrow> bool" |
159 is_final :: "config \<Rightarrow> bool" |
152 where |
160 where |
153 "is_final (s, l, r) = (s = 0)" |
161 "is_final (s, l, r) = (s = 0)" |
154 |
162 |
155 lemma is_final_steps: |
163 lemma is_final_steps: |
156 assumes "is_final (s, l, r)" |
164 assumes "is_final (s, l, r)" |
157 shows "is_final (steps (s, l, r) (p, off) n)" |
165 shows "is_final (steps (s, l, r) (p, off) n)" |
158 using assms by (induct n) (auto) |
166 using assms by (induct n) (auto) |
159 |
167 |
160 fun |
168 |
161 holds_for :: "(tape \<Rightarrow> bool) \<Rightarrow> config \<Rightarrow> bool" ("_ holds'_for _" [100, 99] 100) |
|
162 where |
|
163 "P holds_for (s, l, r) = P (l, r)" |
|
164 |
|
165 lemma is_final_holds[simp]: |
|
166 assumes "is_final c" |
|
167 shows "Q holds_for (steps c (p, off) n) = Q holds_for c" |
|
168 using assms |
|
169 apply(induct n) |
|
170 apply(auto) |
|
171 apply(case_tac [!] c) |
|
172 apply(auto) |
|
173 done |
|
174 |
|
175 type_synonym assert = "tape \<Rightarrow> bool" |
|
176 |
|
177 definition |
|
178 assert_imp :: "assert \<Rightarrow> assert \<Rightarrow> bool" ("_ \<mapsto> _" [0, 0] 100) |
|
179 where |
|
180 "P \<mapsto> Q \<equiv> \<forall>l r. P (l, r) \<longrightarrow> Q (l, r)" |
|
181 |
|
182 lemma holds_for_imp: |
|
183 assumes "P holds_for c" |
|
184 and "P \<mapsto> Q" |
|
185 shows "Q holds_for c" |
|
186 using assms unfolding assert_imp_def |
|
187 by (case_tac c) (auto) |
|
188 |
|
189 definition |
|
190 Hoare :: "assert \<Rightarrow> tprog0 \<Rightarrow> assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" 50) |
|
191 where |
|
192 "{P} p {Q} \<equiv> |
|
193 (\<forall>l r. P (l, r) \<longrightarrow> (\<exists>n. is_final (steps0 (1, (l, r)) p n) \<and> Q holds_for (steps0 (1, (l, r)) p n)))" |
|
194 |
|
195 lemma HoareI: |
|
196 assumes "\<And>l r. P (l, r) \<Longrightarrow> \<exists>n. is_final (steps0 (1, (l, r)) p n) \<and> Q holds_for (steps0 (1, (l, r)) p n)" |
|
197 shows "{P} p {Q}" |
|
198 unfolding Hoare_def using assms by auto |
|
199 |
|
200 |
|
201 lemma step_0 [simp]: |
|
202 shows "step (0, (l, r)) p = (0, (l, r))" |
|
203 by (case_tac p, simp) |
|
204 |
|
205 lemma steps_0 [simp]: |
|
206 shows "steps (0, (l, r)) p n = (0, (l, r))" |
|
207 by (induct n) (simp_all) |
|
208 |
169 |
209 (* if the machine is in the halting state, there must have |
170 (* if the machine is in the halting state, there must have |
210 been a state just before the halting state *) |
171 been a state just before the halting state *) |
211 lemma before_final: |
172 lemma before_final: |
212 assumes "steps0 (1, tp) A n = (0, tp')" |
173 assumes "steps0 (1, tp) A n = (0, tp')" |
478 = (0, l', r')" |
439 = (0, l', r')" |
479 using t_merge_second_same[where s = "0"] |
440 using t_merge_second_same[where s = "0"] |
480 apply(auto) |
441 apply(auto) |
481 done |
442 done |
482 |
443 |
483 |
|
484 text {* |
|
485 {P1} A {Q1} {P2} B {Q2} Q1 \<mapsto> P2 |
|
486 ----------------------------------- |
|
487 {P1} A |+| B {Q2} |
|
488 *} |
|
489 |
|
490 |
|
491 lemma Hoare_plus_halt: |
|
492 assumes aimpb: "Q1 \<mapsto> P2" |
|
493 and A_wf : "tm_wf (A, 0)" |
|
494 and B_wf : "tm_wf (B, 0)" |
|
495 and A_halt : "{P1} A {Q1}" |
|
496 and B_halt : "{P2} B {Q2}" |
|
497 shows "{P1} A |+| B {Q2}" |
|
498 proof(rule HoareI) |
|
499 fix l r |
|
500 assume h: "P1 (l, r)" |
|
501 then obtain n1 |
|
502 where "is_final (steps0 (1, l, r) A n1)" and "Q1 holds_for (steps0 (1, l, r) A n1)" |
|
503 using A_halt unfolding Hoare_def by auto |
|
504 then obtain l' r' where "steps0 (1, l, r) A n1 = (0, l', r')" and c: "Q1 holds_for (0, l', r')" |
|
505 by(case_tac "steps0 (1, l, r) A n1") (auto) |
|
506 then obtain stpa where d: "steps0 (1, l, r) (A |+| B) stpa = (Suc (length A div 2), l', r')" |
|
507 using A_wf by(rule_tac t_merge_pre_halt_same) (auto) |
|
508 moreover |
|
509 from c aimpb have "P2 holds_for (0, l', r')" |
|
510 by (rule holds_for_imp) |
|
511 then have "P2 (l', r')" by auto |
|
512 then obtain n2 |
|
513 where "is_final (steps0 (1, l', r') B n2)" and "Q2 holds_for (steps0 (1, l', r') B n2)" |
|
514 using B_halt unfolding Hoare_def by auto |
|
515 then obtain l'' r'' where "steps0 (1, l', r') B n2 = (0, l'', r'')" and g: "Q2 holds_for (0, l'', r'')" |
|
516 by (case_tac "steps0 (1, l', r') B n2", auto) |
|
517 then have "steps0 (Suc (length A div 2), l', r') (A |+| B) n2 = (0, l'', r'')" |
|
518 by (rule_tac t_merge_second_halt_same) (auto simp: A_wf B_wf) |
|
519 ultimately show |
|
520 "\<exists>n. is_final (steps0 (1, l, r) (A |+| B) n) \<and> Q2 holds_for (steps0 (1, l, r) (A |+| B) n)" |
|
521 using g |
|
522 apply(rule_tac x = "stpa + n2" in exI) |
|
523 apply(simp add: steps_add) |
|
524 done |
|
525 qed |
|
526 |
|
527 definition |
|
528 Hoare_unhalt :: "assert \<Rightarrow> tprog0 \<Rightarrow> bool" ("({(1_)}/ (_))" 50) |
|
529 where |
|
530 "{P} p \<equiv> |
|
531 (\<forall>l r. P (l, r) \<longrightarrow> (\<forall> n . \<not> (is_final (steps0 (1, (l, r)) p n))))" |
|
532 |
|
533 lemma Hoare_unhalt_I: |
|
534 assumes "\<And>l r. P (l, r) \<Longrightarrow> \<forall> n. \<not> is_final (steps0 (1, (l, r)) p n)" |
|
535 shows "{P} p" |
|
536 unfolding Hoare_unhalt_def using assms by auto |
|
537 |
|
538 lemma Hoare_plus_unhalt: |
|
539 fixes A B :: tprog0 |
|
540 assumes aimpb: "Q1 \<mapsto> P2" |
|
541 and A_wf : "tm_wf (A, 0)" |
|
542 and B_wf : "tm_wf (B, 0)" |
|
543 and A_halt : "{P1} A {Q1}" |
|
544 and B_uhalt : "{P2} B" |
|
545 shows "{P1} (A |+| B)" |
|
546 proof(rule_tac Hoare_unhalt_I) |
|
547 fix l r |
|
548 assume h: "P1 (l, r)" |
|
549 then obtain n1 where a: "is_final (steps0 (1, l, r) A n1)" and b: "Q1 holds_for (steps0 (1, l, r) A n1)" |
|
550 using A_halt unfolding Hoare_def by auto |
|
551 then obtain l' r' where "steps0 (1, l, r) A n1 = (0, l', r')" and c: "Q1 holds_for (0, l', r')" |
|
552 by(case_tac "steps0 (1, l, r) A n1", auto) |
|
553 then obtain stpa where d: "steps0 (1, l, r) (A |+| B) stpa = (Suc (length A div 2), l', r')" |
|
554 using A_wf |
|
555 by(rule_tac t_merge_pre_halt_same, auto) |
|
556 from c aimpb have "P2 holds_for (0, l', r')" |
|
557 by(rule holds_for_imp) |
|
558 from this have "P2 (l', r')" by auto |
|
559 from this have e: "\<forall> n. \<not> is_final (steps0 (Suc 0, l', r') B n) " |
|
560 using B_uhalt unfolding Hoare_unhalt_def |
|
561 by auto |
|
562 from e show "\<forall>n. \<not> is_final (steps0 (1, l, r) (A |+| B) n)" |
|
563 proof(rule_tac allI, case_tac "n > stpa") |
|
564 fix n |
|
565 assume h2: "stpa < n" |
|
566 hence "\<not> is_final (steps0 (Suc 0, l', r') B (n - stpa))" |
|
567 using e |
|
568 apply(erule_tac x = "n - stpa" in allE) by simp |
|
569 then obtain s'' l'' r'' where f: "steps0 (Suc 0, l', r') B (n - stpa) = (s'', l'', r'')" and g: "s'' \<noteq> 0" |
|
570 apply(case_tac "steps0 (Suc 0, l', r') B (n - stpa)", auto) |
|
571 done |
|
572 have k: "steps0 (Suc (length A div 2), l', r') (A |+| B) (n - stpa) = (s''+ length A div 2, l'', r'') " |
|
573 using A_wf B_wf f g |
|
574 apply(drule_tac t_merge_second_same, auto) |
|
575 done |
|
576 show "\<not> is_final (steps0 (1, l, r) (A |+| B) n)" |
|
577 proof - |
|
578 have "\<not> is_final (steps0 (1, l, r) (A |+| B) (stpa + (n - stpa)))" |
|
579 using d k A_wf |
|
580 apply(simp only: steps_add d, simp add: tm_wf.simps) |
|
581 done |
|
582 thus "\<not> is_final (steps0 (1, l, r) (A |+| B) n)" |
|
583 using h2 by simp |
|
584 qed |
|
585 next |
|
586 fix n |
|
587 assume h2: "\<not> stpa < n" |
|
588 with d show "\<not> is_final (steps0 (1, l, r) (A |+| B) n)" |
|
589 apply(auto) |
|
590 apply(subgoal_tac "\<exists> d. stpa = n + d", auto) |
|
591 apply(case_tac "(steps0 (Suc 0, l, r) (A |+| B) n)", simp) |
|
592 apply(rule_tac x = "stpa - n" in exI, simp) |
|
593 done |
|
594 qed |
|
595 qed |
|
596 |
444 |
597 end |
445 end |
598 |
446 |